Changeset 1600 for src/ASM/Util.ma

Timestamp:

Dec 13, 2011, 1:41:08 PM (8 years ago)

Author:

sacerdot

Message:

utilities and ASM ported to the new standard library

File:

• src/ASM/Util.ma (modified) (2 diffs)

src/ASM/Util.ma

@@ -2 +2 @@
 include "basics/types.ma".
 include "arithmetics/nat.ma".
-include "ASM/JMCoercions.ma".
+include "basics/russell.ma".
 
 (* let's implement a daemon not used by automation *)
@@ -271 +271 @@
   [ 1: normalize %
   | 2: normalize %
-  | 3: normalize
-       generalize in match (sig2 … (reduce_strong A B tl tl1));
-       >p2 >p3 >p4 normalize in ⊢ (% → ?);
-       #HYP //
-  ]
-qed. 
+  | 3: normalize >p3 in p2; >p4 cases (reduce_strong … tl tl1) normalize
+       #X #H #EQ destruct // ]
+qed.
     
 let rec map2_opt