Changeset 798 for src/Clight/CexecEquiv.ma

Timestamp:

May 13, 2011, 1:10:23 PM (10 years ago)

Author:

campbell

Message:

Fix usual matita tactic mistake.

File:

• src/Clight/CexecEquiv.ma (modified) (1 diff)

src/Clight/CexecEquiv.ma

@@ -367 +367 @@
   | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim
       [ #r ] #F #EXEC whd in EXEC:(??%?); destruct
-  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%?) destruct @refl
+  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%?); destruct @refl
   ]
 | #o #k #i #e #H #EXEC #E destruct