Changeset 3479 for LTS/Language.ma

Timestamp:

Sep 22, 2014, 5:14:56 PM (6 years ago)

Author:

sacerdot

Message:

Repaired.

File:

• LTS/Language.ma (modified) (10 diffs)

LTS/Language.ma

@@ -608 +608 @@
                              | _ ⇒ false
                              ]
-| init_act ⇒ match c2 with [init_act ⇒ true | _ ⇒ false]
 ].
 
@@ -1768 +1767 @@
     * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
     cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta
-    [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) *****
+    [ #x #y #_ (*#_ #_ #_ #H*) *****
     | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1;
       normalize * /2/ ] *
@@ -1868 +1867 @@
         [3: assumption |4: assumption |*:] /3 by nmk/ ]
       % 
-      [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
+      [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
+          >(map_labels_on_trace_append … [lbl]) (*CSC: funzionava prima*)
           whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
           @is_permutation_cons assumption
@@ -1913 +1913 @@
       ]
     ]
-    #seq1 #opt_l #i' #_ #EQcode_s1' change with (m_bind ?????) in ⊢ (??%? → ?);
+    #seq1 #opt_l #i' #_ #EQcode_s1' cases daemon (*CSC: ROTTO QUI
+    change with (m_bind ?????) in ⊢ (??%? → ?);
     inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct]
     * #gen_labs #i'' #EQclean >m_return_bind inversion(opt_l) normalize nodelta
@@ -1941 +1942 @@
           cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
       ]]
-    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
+    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct *)
   | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
     #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
@@ -2277 +2278 @@
   inversion(call_post_clean ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct *****]
   * #gen_labs #i' #EQi' inversion act_lab normalize nodelta
-  [ #f #lab | * [| #lbl1 ]| * [| #nf_l] |] #EQ destruct(EQ) 
+  [ #f #lab | * [| #lbl1 ]| * [| #nf_l]] #EQ destruct(EQ) 
   [1,6: whd in ⊢ (??%% → ?); #EQ destruct ***** 
   |4,5: normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** [2: *] #EQ destruct
@@ -2385 +2386 @@
     cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' 
     #EQenv_it' ***** #EQtrans 
-    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
+    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep cases daemon (*CSC: WAS WORKING
     change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
     [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
@@ -2434 +2435 @@
         ]
     | whd in ⊢ (??%% → ?); #EQ destruct(EQ)
-    ]
+    ] *)
   ]
 | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?;
@@ -2502 +2503 @@
     lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
     cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' #EQenv_it' ***** #EQtrans 
-    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
+    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep cases daemon (*CSC: was working
     change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
     [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
@@ -2630 +2631 @@
        ]
      ]
-]
-qed.
+*)]
+qed.