Changeset 1181


Ignore:
Timestamp:
Sep 5, 2011, 1:11:48 PM (8 years ago)
Author:
mulligan
Message:

changed smallstep exec in order to remove matita bug (superposition.ml on use of auto) when including this file

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r797 r1181  
    6161 | e_step tr s e ⇒ e_step ??? tr s e
    6262 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
    63 #o #i #s #e cases e; //; qed.
     63#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
     64 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
     65  here, used reflexivity instead *)
    6466
    6567axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
Note: See TracChangeset for help on using the changeset viewer.