Backport PR coq#17450: Include env and evar map in ltac backtrace con…

…str for correct printing
Zimmi48 · May 16, 2023 · c3eb858 · c3eb858
2 parents 8768ba3 + 41bfd5f
commit c3eb858
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 12 deletions.
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
@@ -244,9 +244,8 @@ let string_of_call ck =
        | Tacexpr.LtacAtomCall te ->
          Pptactic.pr_glob_tactic (Global.env ())
             (CAst.make (Tacexpr.TacAtom te))
-       | Tacexpr.LtacConstrInterp (c, _) ->
-         let env = Global.env () in
-         pr_glob_constr_env env (Evd.from_env env) c
+       | Tacexpr.LtacConstrInterp (env, sigma, c, _) ->
+         pr_glob_constr_env env sigma c
        | Tacexpr.LtacMLCall te ->
          (Pptactic.pr_glob_tactic (Global.env ())
             te)

diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
@@ -365,7 +365,7 @@ type ltac_call_kind =
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr
   | LtacVarCall of KerName.t option * Id.t * glob_tactic_expr
-  | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map
+  | LtacConstrInterp of Environ.env * Evd.evar_map * Glob_term.glob_constr * Ltac_pretype.ltac_var_map
 
 type ltac_stack = ltac_call_kind Loc.located list
 type ltac_trace = ltac_stack * Geninterp.Val.t Id.Map.t list

diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
@@ -365,7 +365,7 @@ type ltac_call_kind =
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr
   | LtacVarCall of KerName.t option * Id.t * glob_tactic_expr
-  | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map
+  | LtacConstrInterp of Environ.env * Evd.evar_map * Glob_term.glob_constr * Ltac_pretype.ltac_var_map
 
 type ltac_stack = ltac_call_kind Loc.located list
 type ltac_trace = ltac_stack * Geninterp.Val.t Id.Map.t list

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
@@ -600,7 +600,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
     ltac_genargs = ist.lfun;
   } in
   let loc = loc_of_glob_constr term in
-  let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in
+  let trace = push_trace (loc,LtacConstrInterp (env,sigma,term,vars)) ist in
   let (stack, _) = trace in
   (* save and restore the current trace info because the called routine later starts
      with an empty trace *)

diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
@@ -418,7 +418,7 @@ let cvt_stack stack =
         | None -> "" (* anonymous function *)
       in
       fn_name, loc
-    | LtacConstrInterp (c,_) -> "", loc
+    | LtacConstrInterp _ -> "", loc
     ) stack
 
 (* Each list entry contains multiple trace frames. *)
@@ -716,11 +716,7 @@ let explain_ltac_call_trace last trace =
         prtac t ++ str ")"
   | Tacexpr.LtacAtomCall te ->
       quote (prtac (CAst.make (Tacexpr.TacAtom te)))
-  | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) ->
-    (* XXX: This hooks into the CErrors's additional error info API so
-       it is tricky to provide the right env for now. *)
-      let env = Global.env() in
-      let sigma = Evd.from_env env in
+  | Tacexpr.LtacConstrInterp (env, sigma, c, { Ltac_pretype.ltac_constrs = vars }) ->
       quote (Printer.pr_glob_constr_env env sigma c) ++
         (if not (Id.Map.is_empty vars) then
           strbrk " (with " ++

diff --git a/test-suite/bugs/bug_17449.v b/test-suite/bugs/bug_17449.v
@@ -0,0 +1,10 @@
+
+Set Ltac Backtrace.
+
+Ltac foo :=
+  let c := open_constr:(fun x:nat => _) in
+  pose (Prop:Prop) .
+
+Goal True.
+  Fail foo.
+Abort.