Changeset 2701


Ignore:
Timestamp:
Feb 22, 2013, 2:30:43 PM (6 years ago)
Author:
sacerdot
Message:

Automation failure fixed by replacing with hand made proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2699 r2701  
    28752875         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] *)
    28762876         #Hexec whd in Hexec:(??%?); destruct (Hexec) whd @conj try @refl
    2877          /3 by sws_returnstate, swc_call, memext_free_extended_environment/
     2877         (*CSC: auto that used to work for the next two lines, fixed to make
     2878           compiler.ma compile again *)
     2879         @sws_returnstate /3 by swc_call, memext_free_extended_environment/
     2880         [@[] | 2: @swc_call // ]
    28782881    ]
    28792882  | 2: (* Assign statement *)
Note: See TracChangeset for help on using the changeset viewer.