Changeset 698 for src/ASM/Vector.ma


Ignore:
Timestamp:
Mar 18, 2011, 1:47:53 PM (9 years ago)
Author:
mulligan
Message:

Commit with changes to files to get our files to typecheck.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r697 r698  
    88include "basics/types.ma".
    99
    10 include "cerco/Util.ma".
     10include "ASM/Util.ma".
    1111
    1212include "arithmetics/nat.ma".
    1313
    14 include "oldlib/eq.ma".
     14(* include "oldlib/eq.ma". *)
    1515
    1616(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    469469*)
    470470
     471(* dpm: commented out to get out stuff to typecheck
    471472lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
    472473  (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
     
    485486  ]
    486487] qed.
     488*)
    487489
    488490(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.