Changeset 2706


Ignore:
Timestamp:
Feb 22, 2013, 6:23:45 PM (6 years ago)
Author:
mckinna
Message:

repaired contentious broken automation
at end of subgoal 9 of case (* skip *) in main result

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2701 r2706  
    28752875         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] *)
    28762876         #Hexec whd in Hexec:(??%?); destruct (Hexec) whd @conj try @refl
    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 // ]
     2877         (* JHM: do this mostly by hand, to avoid broken automation *)
     2878         @(sws_returnstate ??????? (memext_free_extended_environment …) … (swc_call …)) //
    28812879    ]
    28822880  | 2: (* Assign statement *)
Note: See TracChangeset for help on using the changeset viewer.