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

11 files changed, 191 insertions, 169 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
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 3a4b0571d4..523c7c8305 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -58,6 +58,7 @@ let eval_uconstrs ist cs =
     fail_evar = false;
     expand_evars = true;
     program_mode = false;
+    polymorphic = false;
   } in
   let map c env sigma = c env sigma in
   List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index a348e2cea4..7eb34158e8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -374,20 +374,21 @@ let () = declare_int_option {
   optwrite = fun n -> print_info_trace := n;
 }
 
-let vernac_solve n info tcom b =
+let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
-  let status = Proof_global.with_current_proof (fun etac p ->
-    let with_end_tac = if b then Some etac else None in
-    let global = match n with SelectAll | SelectList _ -> true | _ -> false in
-    let info = Option.append info !print_info_trace in
-    let (p,status) =
-      Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
-    in
-    (* in case a strict subtree was completed,
-       go back to the top of the prooftree *)
-    let p = Proof.maximal_unfocus Vernacentries.command_focus p in
-    p,status) in
-    if not status then Feedback.feedback Feedback.AddedAxiom
+  let pstate, status = Proof_global.with_current_proof (fun etac p ->
+      let with_end_tac = if b then Some etac else None in
+      let global = match n with SelectAll | SelectList _ -> true | _ -> false in
+      let info = Option.append info !print_info_trace in
+      let (p,status) =
+        Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+      in
+      (* in case a strict subtree was completed,
+         go back to the top of the prooftree *)
+      let p = Proof.maximal_unfocus Vernacentries.command_focus p in
+      p,status) pstate in
+  if not status then Feedback.feedback Feedback.AddedAxiom;
+  Some pstate
 
 let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
 
@@ -434,12 +435,12 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false
 }
 
 VERNAC { tactic_mode } EXTEND VernacSolve
-| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     { classify_as_proofstep } -> {
     let g = Option.default (Goal_select.get_default_goal_selector ()) g in
-    vernac_solve g n t def
+    Vernacentries.vernac_require_open_proof vernac_solve g n t def
   }
-| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     {
       let anon_abstracting_tac = is_anonymous_abstract t in
       let solving_tac = is_explicit_terminator t in
@@ -449,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve
       VtLater
     } -> {
       let t = rm_abstract t in
-      vernac_solve Goal_select.SelectAll n t def
+      Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def
     }
 END
 
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index a12dee48a8..de3a9c9fa9 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram
 
 open Obligations
 
-let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
-let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
+let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac)
+let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac)
 
 let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
 
 }
 
 VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl }
-| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, Some name, Some t) tac }
-| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
     { obligation (num, Some name, None) tac }
-| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, None, Some t) tac }
-| [ "Obligation" integer(num) withtac(tac) ] ->
+| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] ->
     { obligation (num, None, None) tac }
-| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
+| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
     { next_obligation (Some name) tac }
-| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
+| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
 END
 
 VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 86a227415a..469551809c 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -180,34 +180,34 @@ TACTIC EXTEND setoid_rewrite
 END
 
 VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None }
 
-  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) None None }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
       { declare_relation atts a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       { declare_relation atts a aeq n None (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
       { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
       { declare_relation atts a aeq n None None (Some lemma3) }
 END
@@ -234,64 +234,64 @@ GRAMMAR EXTEND Gram
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) None None }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None None (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
-         add_setoid atts [] a aeq t n;
+         add_setoid atts [] a aeq t n
      }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
-         add_setoid atts binders a aeq t n;
+         add_setoid atts binders a aeq t n
      }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
     => { VtUnknown, VtNow }
     -> {
-           add_morphism_infer atts m n;
+          add_morphism_infer atts m n
        }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
     -> {
-           add_morphism atts [] m s n;
+          add_morphism atts [] m s n
        }
-  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
+  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
     -> {
-           add_morphism atts binders m s n;
+          add_morphism atts binders m s n
        }
 END
 
@@ -310,7 +310,12 @@ TACTIC EXTEND setoid_transitivity
 END
 
 VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY
-| [ "Print" "Rewrite" "HintDb" preident(s) ] ->
-  { let sigma, env = Pfedit.get_current_context () in
-    Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) }
+| ![ proof ] [ "Print" "Rewrite" "HintDb" preident(s) ] ->
+  { (* This command should not use the proof env, keeping previous
+       behavior as requested in review. *)
+    fun ~pstate ->
+      let sigma, env = Option.cata Pfedit.get_current_context
+          (let e = Global.env () in Evd.from_env e, e) pstate in
+    Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s);
+    pstate }
 END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 1bdba699f7..80070a7493 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1307,7 +1307,6 @@ let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a)
 let register_basic_print0 wit f g h =
   Genprint.register_print0 wit (lift f) (lift g) (lift_top h)
 
-
 let pr_glob_constr_pptac env sigma c =
   pr_glob_constr_env env c
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b1d5c0252f..75565c1a34 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -618,7 +618,9 @@ let solve_remaining_by env sigma holes by =
     in
     (* Only solve independent holes *)
     let indep = List.map_filter map holes in
-    let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
+    let ist = { Geninterp.lfun = Id.Map.empty
+              ; poly = false
+              ; extra = Geninterp.TacStore.empty } in
     let solve_tac = match tac with
     | Genarg.GenArg (Genarg.Glbwit tag, tac) ->
       Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ())
@@ -1790,15 +1792,15 @@ let declare_an_instance n s args =
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
-let anew_instance atts binders instance fields =
+let anew_instance ~pstate atts binders instance fields =
   let program_mode = atts.program in
-  new_instance ~program_mode atts.polymorphic
+  new_instance ~pstate ~program_mode atts.polymorphic
     binders instance (Some (true, CAst.make @@ CRecord (fields)))
     ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info
 
-let declare_instance_refl atts binders a aeq n lemma =
+let declare_instance_refl ~pstate atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
-  in anew_instance atts binders instance
+  in anew_instance ~pstate atts binders instance
        [(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
 
 let declare_instance_sym atts binders a aeq n lemma =
@@ -1811,47 +1813,44 @@ let declare_instance_trans atts binders a aeq n lemma =
   in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "transitivity"),lemma)]
 
-let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
+let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
-  let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
-  in ignore(anew_instance atts binders instance []);
+  let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in
+  let _, pstate = anew_instance ~pstate atts binders instance [] in
   match (refl,symm,trans) with
-      (None, None, None) -> ()
+      (None, None, None) -> pstate
     | (Some lemma1, None, None) ->
-        ignore (declare_instance_refl atts binders a aeq n lemma1)
+      snd @@ declare_instance_refl ~pstate atts binders a aeq n lemma1
     | (None, Some lemma2, None) ->
-        ignore (declare_instance_sym atts binders a aeq n lemma2)
+      snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2
     | (None, None, Some lemma3) ->
-        ignore (declare_instance_trans atts binders a aeq n lemma3)
+      snd @@ declare_instance_trans ~pstate atts binders a aeq n lemma3
     | (Some lemma1, Some lemma2, None) ->
-        ignore (declare_instance_refl atts binders a aeq n lemma1);
-        ignore (declare_instance_sym atts binders a aeq n lemma2)
+      let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
+      snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2
     | (Some lemma1, None, Some lemma3) ->
-        let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
-        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
-	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
-	in ignore(
-            anew_instance atts binders instance
+        let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
+        let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+        let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in
+        snd @@ anew_instance ~pstate atts binders instance
               [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
-               (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)])
+               (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]
     | (None, Some lemma2, Some lemma3) ->
-        let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
-        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
-	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
-	in ignore(
-            anew_instance atts binders instance
+        let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
+        let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+        let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in
+        snd @@ anew_instance ~pstate atts binders instance
               [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
-               (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)])
+               (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]
      | (Some lemma1, Some lemma2, Some lemma3) ->
-        let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
-        let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
-        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
-	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
-	in ignore(
-          anew_instance atts binders instance
+        let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
+        let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
+        let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+        let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in
+        snd @@ anew_instance ~pstate atts binders instance
             [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
              (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
-             (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)])
+             (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]
 
 let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
 
@@ -1947,18 +1946,18 @@ let warn_add_setoid_deprecated =
   CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
       Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation."))
 
-let add_setoid atts binders a aeq t n =
+let add_setoid ~pstate atts binders a aeq t n =
   warn_add_setoid_deprecated ?loc:a.CAst.loc ();
   init_setoid ();
-  let _lemma_refl = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
-  let _lemma_sym = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
-  let _lemma_trans = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+  let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+  let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+  let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
-  in ignore(
-    anew_instance atts binders instance
+  in
+  snd @@ anew_instance ~pstate atts binders instance
       [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
        (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
-       (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+       (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]
 
 
 let make_tactic name =
@@ -1970,7 +1969,7 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer atts m n =
+let add_morphism_infer ~pstate atts m n : Proof_global.t option =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
   (* NB: atts.program is ignored, program mode automatically set by vernacentries *)
@@ -1981,45 +1980,47 @@ let add_morphism_infer atts m n =
     if Lib.is_modtype () then
       let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
-				(Entries.ParameterEntry 
-                                 (None,(instance,uctx),None),
-				 Decl_kinds.IsAssumption Decl_kinds.Logical)
+          (Entries.ParameterEntry
+             (None,(instance,uctx),None),
+           Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
-	add_instance (Typeclasses.new_instance 
-                        (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
-	declare_projection n instance_id (ConstRef cst)
+      add_instance (Typeclasses.new_instance
+                      (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
+      declare_projection n instance_id (ConstRef cst);
+      pstate
     else
       let kind = Decl_kinds.Global, atts.polymorphic,
-	Decl_kinds.DefinitionBody Decl_kinds.Instance 
+                 Decl_kinds.DefinitionBody Decl_kinds.Instance
       in
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
       let hook _ _ _ = function
-	| Globnames.ConstRef cst ->
-	  add_instance (Typeclasses.new_instance 
-			  (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
+        | Globnames.ConstRef cst ->
+          add_instance (Typeclasses.new_instance
+                          (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
                           atts.global (ConstRef cst));
-	  declare_projection n instance_id (ConstRef cst)
-	| _ -> assert false
+          declare_projection n instance_id (ConstRef cst)
+        | _ -> assert false
       in
       let hook = Lemmas.mk_hook hook in
-	Flags.silently
-	  (fun () ->
-            Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance);
-	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
+      Flags.silently
+        (fun () ->
+           let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+           Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) ()
 
-let add_morphism atts binders m s n =
+let add_morphism ~pstate atts binders m s n =
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
   let instance =
     (((CAst.make @@ Name instance_id),None), Explicit,
     CAst.make @@ CAppExpl (
              (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None),
-	     [cHole; s; m]))
+             [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-  ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
-     None
-    ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
+  let _, pstate = new_instance ~pstate ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
+      None
+    ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in
+  pstate
 
 (** Bind to "rewrite" too *)
 
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 2457b265f0..a200cb5ced 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -81,18 +81,18 @@ val cl_rewrite_clause :
 val is_applied_rewrite_relation :
   env -> evar_map -> rel_context -> constr -> types option
 
-val declare_relation : rewrite_attributes ->
+val declare_relation : pstate:Proof_global.t option -> rewrite_attributes ->
   ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
-  constr_expr option -> constr_expr option -> constr_expr option -> unit
+  constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option
 
-val add_setoid :
+val add_setoid : pstate:Proof_global.t option ->
   rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
-  Id.t -> unit
+  Id.t -> Proof_global.t option
 
-val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> unit
+val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option
 
-val add_morphism :
-  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
+val add_morphism : pstate:Proof_global.t option ->
+  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index eac84f0543..4398fb14ab 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -138,9 +138,10 @@ let f_debug : debug_info TacStore.field = TacStore.field ()
 let f_trace : ltac_trace TacStore.field = TacStore.field ()
 
 (* Signature for interpretation: val_interp and interpretation functions *)
-type interp_sign = Geninterp.interp_sign = {
-  lfun : value Id.Map.t;
-  extra : TacStore.t }
+type interp_sign = Geninterp.interp_sign =
+  { lfun : value Id.Map.t
+  ; poly : bool
+  ; extra : TacStore.t }
 
 let extract_trace ist =
   if is_traced () then match TacStore.get ist.extra f_trace with
@@ -544,12 +545,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
   let (_, dummy_proofview) = Proofview.init sigma [] in
 
   (* Again this is called at times with no open proof! *)
-  let name, poly =
-    try
-      let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in
-      name, poly
-    with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false
-  in
+  let name, poly = Id.of_string "tacinterp", ist.poly in
   let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
   let (evd,c) =
     catch_error trace (understand_ltac flags env sigma vars kind) term
@@ -566,11 +562,13 @@ let constr_flags () = {
   fail_evar = true;
   expand_evars = true;
   program_mode = false;
+  polymorphic = false;
 }
 
 (* Interprets a constr; expects evars to be solved *)
 let interp_constr_gen kind ist env sigma c =
-  interp_gen kind ist false (constr_flags ()) env sigma c
+  let flags = { (constr_flags ()) with polymorphic = ist.Geninterp.poly } in
+  interp_gen kind ist false flags env sigma c
 
 let interp_constr = interp_constr_gen WithoutTypeConstraint
 
@@ -582,6 +580,7 @@ let open_constr_use_classes_flags () = {
   fail_evar = false;
   expand_evars = true;
   program_mode = false;
+  polymorphic = false;
 }
 
 let open_constr_no_classes_flags () = {
@@ -590,6 +589,7 @@ let open_constr_no_classes_flags () = {
   fail_evar = false;
   expand_evars = true;
   program_mode = false;
+  polymorphic = false;
 }
 
 let pure_open_constr_flags = {
@@ -598,6 +598,7 @@ let pure_open_constr_flags = {
   fail_evar = false;
   expand_evars = false;
   program_mode = false;
+  polymorphic = false;
 }
 
 (* Interprets an open constr *)
@@ -1021,6 +1022,7 @@ let type_uconstr ?(flags = (constr_flags ()))
     ltac_idents = closure.idents;
     ltac_genargs = Id.Map.empty;
   } in
+  let flags = { flags with polymorphic = ist.Geninterp.poly } in
   understand_ltac flags env sigma vars expected_type term
   end
 
@@ -1146,6 +1148,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   (* For extensions *)
   | TacAlias {loc; v=(s,l)} ->
       let alias = Tacenv.interp_alias s in
+      Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
       let (>>=) = Ftactic.bind in
       let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
       let tac l =
@@ -1153,8 +1156,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
         let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in
         Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
         let ist = {
-          lfun = lfun;
-          extra = TacStore.set ist.extra f_trace trace; } in
+          lfun
+        ; poly
+        ; extra = TacStore.set ist.extra f_trace trace } in
         val_interp ist alias.Tacenv.alias_body >>= fun v ->
         Ftactic.lift (tactic_of_value ist v)
       in
@@ -1207,12 +1211,13 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
       if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v
       end
   | ArgArg (loc,r) ->
+      Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
       let ids = extract_ids [] ist.lfun Id.Set.empty in
       let loc_info = (Option.default loc loc',LtacNameCall r) in
       let extra = TacStore.set ist.extra f_avoid_ids ids in
       push_trace loc_info ist >>= fun trace ->
       let extra = TacStore.set extra f_trace trace in
-      let ist = { lfun = Id.Map.empty; extra = extra; } in
+      let ist = { lfun = Id.Map.empty; poly; extra } in
       let appl = GlbAppl[r,[]] in
       Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
         (val_interp ~appl ist (Tacenv.interp_ltac r))
@@ -1260,6 +1265,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
 
 (* Interprets an application node *)
 and interp_app loc ist fv largs : Val.t Ftactic.t =
+  Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
   let (>>=) = Ftactic.bind in
   let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in
   if has_type fv (topwit wit_tacvalue) then
@@ -1277,9 +1283,11 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
       if List.is_empty lvar then
         begin wrap_error
             begin
-              let ist = {
-                lfun = newlfun;
-                extra = TacStore.set ist.extra f_trace []; } in
+              let ist =
+                { lfun = newlfun
+                ; poly
+                ; extra = TacStore.set ist.extra f_trace []
+                } in
               Profile_ltac.do_profile "interp_app" trace ~count_call:false
                 (catch_error_tac trace (val_interp ist body)) >>= fun v ->
               Ftactic.return (name_vfun (push_appl appl largs) v)
@@ -1317,8 +1325,10 @@ and tactic_of_value ist vle =
   if has_type vle (topwit wit_tacvalue) then
   match to_tacvalue vle with
   | VFun (appl,trace,lfun,[],t) ->
+    Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
       let ist = {
         lfun = lfun;
+        poly;
         extra = TacStore.set ist.extra f_trace []; } in
       let tac = name_if_glob appl (eval_tactic ist t) in
       Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
@@ -1388,6 +1398,7 @@ and interp_letin ist llc u =
 (** [interp_match_success lz ist succ] interprets a single matching success
     (of type {!Tactic_matching.t}). *)
 and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
+  Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
   let (>>=) = Ftactic.bind in
   let lctxt = Id.Map.map interp_context context in
   let hyp_subst = Id.Map.map Value.of_constr terms in
@@ -1396,9 +1407,11 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
   val_interp ist lhs >>= fun v ->
   if has_type v (topwit wit_tacvalue) then match to_tacvalue v with
   | VFun (appl,trace,lfun,[],t) ->
-      let ist = {
-        lfun = lfun;
-        extra = TacStore.set ist.extra f_trace trace; } in
+      let ist =
+        { lfun = lfun
+        ; poly
+        ; extra = TacStore.set ist.extra f_trace trace
+        } in
       let tac = eval_tactic ist t in
       let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in
       catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy))
@@ -1872,7 +1885,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
 
 let default_ist () =
   let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
-  { lfun = Id.Map.empty; extra = extra }
+  { lfun = Id.Map.empty; poly = false; extra = extra }
 
 let eval_tactic t =
   Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *)
@@ -1912,11 +1925,12 @@ end
 
 
 let interp_tac_gen lfun avoid_ids debug t =
+  Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let extra = TacStore.set TacStore.empty f_debug debug in
   let extra = TacStore.set extra f_avoid_ids avoid_ids in
-  let ist = { lfun = lfun; extra = extra } in
+  let ist = { lfun; poly; extra } in
   let ltacvars = Id.Map.domain lfun in
   interp_tactic ist
     (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
@@ -2057,20 +2071,15 @@ let interp_redexp env sigma r =
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
 let _ =
-  let eval lfun env sigma ty tac =
+  let eval lfun poly env sigma ty tac =
     let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
-    let ist = { lfun = lfun; extra; } in
+    let ist = { lfun; poly; extra; } in
     let tac = interp_tactic ist tac in
-    (* XXX: This depends on the global state which is bad; the hooking
-       mechanism should be modified. *)
-    let name, poly =
-      try
-        let (_, poly, _) = Proof_global.get_current_persistence () in
-        let name = Proof_global.get_current_proof_name () in
-        name, poly
-      with | Proof_global.NoCurrentProof ->
-        Id.of_string "ltac_gen", false
-    in
+    (* EJGA: We sould also pass the proof name if desired, for now
+       poly seems like enough to get reasonable behavior in practice
+     *)
+    let name, poly = Id.of_string "ltac_gen", poly in
+    let name, poly = Id.of_string "ltac_gen", poly in
     let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index d9c80bb835..22a092fa8b 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -39,9 +39,10 @@ module TacStore : Store.S with
   and type 'a field = 'a Geninterp.TacStore.field
 
 (** Signature for interpretation: val\_interp and interpretation functions *)
-type interp_sign = Geninterp.interp_sign = {
-  lfun : value Id.Map.t;
-  extra : TacStore.t }
+type interp_sign = Geninterp.interp_sign =
+  { lfun : value Id.Map.t
+  ; poly : bool
+  ; extra : TacStore.t }
 
 open Genintern
 
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 52a83a038f..04f3116664 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -370,7 +370,10 @@ let explain_ltac_call_trace last trace loc =
           strbrk " (with " ++
             prlist_with_sep pr_comma
             (fun (id,c) ->
-              let sigma, env = Pfedit.get_current_context () in
+              (* XXX: This hooks into the ExplainErr extension API
+                 so it is tricky to provide the right env for now. *)
+              let env = Global.env () in
+              let sigma = Evd.from_env env in
               Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c)
             (List.rev (Id.Map.bindings vars)) ++ str ")"
         else mt())