Changeset 1566 for src/Clight/CexecComplete.ma

Timestamp:

Nov 25, 2011, 6:12:47 PM (9 years ago)

Author:

campbell

Message:

Pacify changes to destruct tactic.

File:

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

src/Clight/CexecComplete.ma

@@ -123 +123 @@
   P e.
 #ge #env #m #e #ty #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H)
-[ #id #l #ty #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
-| #id #sp #l #ty #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
-| #e #ty #sp #l #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
-| #e #id #ty #l #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
-| #e #id #ty #l #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
+[ #id #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
+| #id #sp #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
+| #e' #ty' #sp #l' #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
+| #e' #id #ty' #l' #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
+| #e' #id #ty' #l' #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
 ] qed.