3 files changed, 38 insertions, 9 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 47f593ff3e..ffd8b71e5d 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -50,7 +50,8 @@ let with_delayed_uconstr ist c tac =
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
     fail_evar = false;
-    expand_evars = true
+    expand_evars = true;
+    program_mode = false;
  } in
   let c = Tacinterp.type_uconstr ~flags ist c in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
@@ -344,7 +345,9 @@ let constr_flags () = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
   Pretyping.fail_evar = false;
-  Pretyping.expand_evars = true }
+  Pretyping.expand_evars = true;
+  Pretyping.program_mode = false;
+}
 
 let refine_tac ist simple with_classes c =
   Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 7be8f67616..663537f3e8 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -56,7 +56,8 @@ let eval_uconstrs ist cs =
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
     fail_evar = false;
-    expand_evars = true
+    expand_evars = true;
+    program_mode = 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/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 3e7479903a..62906303a4 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -530,7 +530,15 @@ let interp_gen kind ist pattern_mode flags env sigma c =
       invariant that running the tactic returned by push_trace does
       not modify sigma. *)
   let (_, dummy_proofview) = Proofview.init sigma [] in
-  let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview 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 (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
   in
@@ -544,7 +552,9 @@ let constr_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
   fail_evar = true;
-  expand_evars = true }
+  expand_evars = true;
+  program_mode = false;
+}
 
 (* Interprets a constr; expects evars to be solved *)
 let interp_constr_gen kind ist env sigma c =
@@ -558,19 +568,25 @@ let open_constr_use_classes_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = true }
+  expand_evars = true;
+  program_mode = false;
+}
 
 let open_constr_no_classes_flags () = {
   use_typeclasses = false;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = true }
+  expand_evars = true;
+  program_mode = false;
+}
 
 let pure_open_constr_flags = {
   use_typeclasses = false;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = false }
+  expand_evars = false;
+  program_mode = false;
+}
 
 (* Interprets an open constr *)
 let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c =
@@ -2033,7 +2049,16 @@ let _ =
     let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
     let ist = { lfun = lfun; extra; } in
     let tac = interp_tactic ist tac in
-    let name, poly = Id.of_string "ltac_sub", false 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
     let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in