Changeset 889 for src

Timestamp:

Jun 6, 2011, 11:07:24 PM (10 years ago)

Author:

sacerdot

Message:

Minor changes because of the new, weaker (but much faster) delift.

Location:

src

Files:

• ASM/AssemblyProof.ma (modified) (2 diffs)
• ASM/Vector.ma (modified) (1 diff)
• common/Integers.ma (modified) (2 diffs)

src/ASM/AssemblyProof.ma

@@ -762 +762 @@
      @eq_instruction_refl
    | cases arg -i arg;
+(*  
+16,17,18,19,20,28,19
+*)
      [1,2,3: #arg1 #arg2
        @(list_addressing_mode_tags_elim_prop … arg1) whd try %
@@ -833 +836 @@
        >half_add_SO
        >lookup_insert_hit
-       >lookup_insert_miss try @not_eqvb_SS
+       >lookup_insert_miss //
        >lookup_insert_hit
        normalize

src/ASM/Vector.ma

@@ -338 +338 @@
     | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
     ].
-> plus_n_Sm_fast @refl qed.
+< plus_n_Sm_fast @refl qed.
 
 let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝

src/common/Integers.ma

@@ -434 +434 @@
 theorem eq_sym:
   ∀x,y. eq x y = eq y x.
-#x #y @eq_bv_elim @eq_bv_elim /2/
+#x #y change with (eq_bv ??? = eq_bv ???)
+ @eq_bv_elim @eq_bv_elim /2/
 [ #NE #E @False_ind >E in NE * /2/
 | #E #NE @False_ind >E in NE * /2/
@@ -440 +441 @@
 
 theorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y).
-#x #y @eq_bv_elim #H @H qed.
+#x #y change with (if eq_bv ? x y then ? else ?) @eq_bv_elim #H @H qed.
 
 theorem eq_true: ∀x. eq x x = true.