Changeset 1516 for src/joint/BEValues.ma

Timestamp:

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

Author:

sacerdot

Message:

Ported to syntax of Matita 0.99.1.

File:

• src/joint/BEValues.ma (modified) (2 diffs)

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.