Changeset 1521 for src/utilities/binary

Timestamp:

Nov 21, 2011, 1:06:01 PM (9 years ago)

Author:

sacerdot

Message:

Syntax change in Matita: change what where => change where what.

File:

• src/utilities/binary/Z.ma (modified) (1 diff)

src/utilities/binary/Z.ma

@@ -522 +522 @@
 [ //;
 | #m' >Zpred_pos_succ
-    change in ⊢ (??(??%)?); with (Zsucc (pos m'))
+    change with (Zsucc (pos m')) in ⊢ (??(??%)?);
     <Zpred_Zplus_neg_O >Zpred_Zsucc @refl
 | #m' whd in ⊢ (??%%); >pos_compare_S_one normalize;