Changeset 1521 for src/Cminor

Timestamp:

Nov 21, 2011, 1:06:01 PM (8 years ago)

Author:

sacerdot

Message:

Syntax change in Matita: change what where => change where what.

File:

• src/Cminor/toRTLabs.ma (modified) (4 diffs)

src/Cminor/toRTLabs.ma

@@ -28 +28 @@
       whd in E:(??%?); destruct;
       whd >lookup_add_hit % #A destruct
-    | #H change in E:(??(match % with [ _ ⇒ ? ])?); with (populate_env e u tl)
+    | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?);
       lapply (refl ? (populate_env e u tl))
       cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
@@ -44 +44 @@
 [ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
 | * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
-  change in E:(??(match % with [ _ ⇒ ?])?); with (populate_env e u tl)
+  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
   lapply (refl ? (populate_env e u tl))
   cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
@@ -65 +65 @@
 [ #lbls #u #lbls' #u' #E #l *
 | #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
-  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)
+  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
   lapply (refl ? (populate_label_env lbls u t))
   cases (populate_label_env lbls u t) in ⊢ (???% → %);
@@ -82 +82 @@
 [ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
 | #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
-  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)
+  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
   lapply (refl ? (populate_label_env lbls u t))
   cases (populate_label_env lbls u t) in ⊢ (???% → %);