From bd5689d4e9294d66b3eb4ecdc0af3ad7d65fe52d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 26 Oct 2018 10:05:58 +0200
Subject: [coqpp] [ltac] Adapt to removal of imperative proof state.

We add state handling to tactics.

TODO:

- [rewrite] `add_morphism_infer` creates problems as it opens a proof.
- [g_obligations] with_tac
---
 plugins/ltac/extratactics.mlg | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'plugins/ltac/extratactics.mlg')

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0428f08138..8bcf85b04a 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -813,9 +813,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 +913,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 +945,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 +1098,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
-- 
cgit v1.2.3


From c0cff3a7ebb79d1142090108c56e9aa64c3b481d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 13 Feb 2019 05:37:09 +0100
Subject: [geninterp] Track polymorphic status in tactic interpretation.

---
 plugins/ltac/extratactics.mlg | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'plugins/ltac/extratactics.mlg')

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 8bcf85b04a..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 =
-- 
cgit v1.2.3