aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
-rw-r--r--plugins/ltac/tacinterp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 00ac155f0e..f2241e78d2 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -773,7 +773,7 @@ let interp_may_eval f ist env sigma = function
function already use effect, I call [run] hoping it doesn't mess
up with any assumption. *)
Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () ->
- str"interpretation of term " ++ pr_glob_constr_env env (fst c)));
+ str"interpretation of term " ++ pr_glob_constr_env env sigma (fst c)));
Exninfo.iraise reraise
(* Interprets a constr expression possibly to first evaluate *)