Changeset 1516 for src/joint

Timestamp:

Nov 19, 2011, 12:38:20 AM (9 years ago)

Author:

sacerdot

Message:

Ported to syntax of Matita 0.99.1.

Location:

src/joint

Files:

• BEValues.ma (modified) (2 diffs)
• TranslateUtils.ma (modified) (1 diff)

src/joint/BEValues.ma

@@ -74 +74 @@
   [ O ⇒ λ_.[]
   | S m ⇒ λpr':n=S m.(BVptr p (mk_part … part …))::bevals_of_pointer_aux p (S part) m ?] (refl ? n).
-/3/ qed.
+/3/ (*Andrea: by _ cannot be re-parsed*) qed.
 
 definition bevals_of_pointer: pointer → list beval ≝
@@ -84 +84 @@
 * * #pbl #pok #poff
 try %
-whd in ⊢ (??%?) >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %]
-whd in ⊢ (??%?) >reflexive_eq_pointer >(eqb_n_n 2) %
+whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %]
+whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 2) %
 qed.
 

src/joint/TranslateUtils.ma

@@ -21 +21 @@
  #pars0 #globals #def #n elim n
   [ %
-  | #m whd in ⊢ (? → ??(??%)?) whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?) 
+  | #m whd in ⊢ (? → ??(??%)?); whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?) ;
     cases (fresh_regs pars0 globals def m) normalize nodelta
-    #def' #regs #EQ change in EQ with (|regs| = m) <EQ
+    #def' #regs #EQ change in EQ; with (|regs| = m) <EQ
     @refl
  ]