Changeset 2706 for src/Clight/switchRemoval.ma

Timestamp:

Feb 22, 2013, 6:23:45 PM (8 years ago)

Author:

mckinna

Message:

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

File:

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

src/Clight/switchRemoval.ma

@@ -2875 +2875 @@
          | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] *)
          #Hexec whd in Hexec:(??%?); destruct (Hexec) whd @conj try @refl
-         (*CSC: auto that used to work for the next two lines, fixed to make
-           compiler.ma compile again *)
-         @sws_returnstate /3 by swc_call, memext_free_extended_environment/
-         [@[] | 2: @swc_call // ]
+         (* JHM: do this mostly by hand, to avoid broken automation *)
+         @(sws_returnstate ??????? (memext_free_extended_environment …) … (swc_call …)) //
     ]
   | 2: (* Assign statement *)