Merge PR #9129: [proof] Removal of imperative state ; interpretation layers only.

Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes

1 files changed, 10 insertions, 8 deletions

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0428f08138..f5098d2a34 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -53,6 +53,7 @@ let with_delayed_uconstr ist c tac =
     fail_evar = false;
     expand_evars = true;
     program_mode = false;
+    polymorphic = false;
  } in
   let c = Tacinterp.type_uconstr ~flags ist c in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
@@ -348,6 +349,7 @@ let constr_flags () = {
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true;
   Pretyping.program_mode = false;
+  Pretyping.polymorphic = false;
 }
 
 let refine_tac ist simple with_classes c =
@@ -813,9 +815,9 @@ END
 
 TACTIC EXTEND transparent_abstract
 | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl ->
-      Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end }
+    Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end; }
 | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl ->
-      Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end }
+    Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end; }
 END
 
 (* ********************************************************************* *)
@@ -913,9 +915,9 @@ END
    the semantics of the LCF-style tactics, hence with the classic tactic
    mode. *)
 VERNAC COMMAND EXTEND GrabEvars
-| [ "Grab" "Existential" "Variables" ]
+| ![ proof ] [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
-  -> { Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p) }
+  -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p)) pstate }
 END
 
 (* Shelves all the goals under focus. *)
@@ -945,9 +947,9 @@ END
 
 (* Command to add every unshelved variables to the focus *)
 VERNAC COMMAND EXTEND Unshelve
-| [ "Unshelve" ]
+| ![ proof ] [ "Unshelve" ]
   => { classify_as_proofstep }
-  -> { Proof_global.simple_with_current_proof (fun _ p  -> Proof.unshelve p) }
+  -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p  -> Proof.unshelve p)) pstate  }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
@@ -1098,8 +1100,8 @@ END
 
 
 VERNAC COMMAND EXTEND OptimizeProof
-| [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
-  { Proof_global.compact_the_proof () }
+| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
+  { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate }
 | [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
   { Gc.compact () }
 END