5 files changed, 16 insertions, 12 deletions
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 5d49d1635c..01b1025da1 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1100,7 +1100,7 @@ let interp_constr flags ist c =
 let () =
   let intern = intern_constr in
   let interp ist c = interp_constr constr_flags ist c in
-  let print env c = str "constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in
+  let print env sigma c = str "constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
   let obj = {
     ml_intern = intern;
@@ -1113,7 +1113,7 @@ let () =
 let () =
   let intern = intern_constr in
   let interp ist c = interp_constr open_constr_no_classes_flags ist c in
-  let print env c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in
+  let print env sigma c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
   let obj = {
     ml_intern = intern;
@@ -1125,7 +1125,7 @@ let () =
 
 let () =
   let interp _ id = return (Value.of_ident id) in
-  let print _ id = str "ident:(" ++ Id.print id ++ str ")" in
+  let print _ _ id = str "ident:(" ++ Id.print id ++ str ")" in
   let obj = {
     ml_intern = (fun _ _ id -> GlbVal id, gtypref t_ident);
     ml_interp = interp;
@@ -1147,7 +1147,7 @@ let () =
     let sigma = Evd.from_env env in
     Patternops.subst_pattern env sigma subst c
   in
-  let print env pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env Evd.empty pat ++ str ")" in
+  let print env sigma pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env sigma pat ++ str ")" in
   let interp _ c = return (Value.of_pattern c) in
   let obj = {
     ml_intern = intern;
@@ -1169,7 +1169,7 @@ let () =
     return (Value.of_ext val_preterm c)
   in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
-  let print env c = str "preterm:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in
+  let print env sigma c = str "preterm:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in
   let obj = {
     ml_intern = (fun _ _ e -> Empty.abort e);
     ml_interp = interp;
@@ -1193,7 +1193,7 @@ let () =
   in
   let subst s c = Globnames.subst_global_reference s c in
   let interp _ gr = return (Value.of_reference gr) in
-  let print _ = function
+  let print _ _ = function
   | GlobRef.VarRef id -> str "reference:(" ++ str "&" ++ Id.print id ++ str ")"
   | r -> str "reference:(" ++ Printer.pr_global r ++ str ")"
   in
@@ -1241,7 +1241,7 @@ let () =
       return (Tac2ffi.of_closure (Tac2ffi.abstract len clos))
   in
   let subst s (ids, tac) = (ids, Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in
-  let print env (ids, tac) =
+  let print env sigma (ids, tac) =
     let ids =
       if List.is_empty ids then mt ()
       else pr_sequence Id.print ids ++ spc () ++ str "|-" ++ spc ()
@@ -1290,7 +1290,7 @@ let () =
       return (Tac2ffi.of_closure (Tac2ffi.abstract len clos))
   in
   let subst s (ids, tac) = (ids, Genintern.substitute Tacarg.wit_tactic s tac) in
-  let print env (ids, tac) =
+  let print env sigma (ids, tac) =
     let ids =
       if List.is_empty ids then mt ()
       else pr_sequence Id.print ids ++ str " |- "
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index eebd6635fa..d0655890a7 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -853,8 +853,10 @@ let pr_frame = function
   str "Prim <" ++ str ml.mltac_plugin ++ str ":" ++ str ml.mltac_tactic ++ str ">"
 | FrExtn (tag, arg) ->
   let obj = Tac2env.interp_ml_object tag in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   str "Extn " ++ str (Tac2dyn.Arg.repr tag) ++ str ":" ++ spc () ++
-    obj.Tac2env.ml_print (Global.env ()) arg
+    obj.Tac2env.ml_print env sigma arg
 
 let () = register_handler begin function
 | Tac2interp.LtacError (kn, args) ->
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index 6c2133f8f2..f6d07e484b 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -253,7 +253,7 @@ type ('a, 'b) ml_object = {
   ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun;
   ml_subst : Mod_subst.substitution -> 'b -> 'b;
   ml_interp : environment -> 'b -> valexpr Proofview.tactic;
-  ml_print : Environ.env -> 'b -> Pp.t;
+  ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
 }
 
 module MLTypeObj =
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index 2468959810..af1197c24c 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -122,7 +122,7 @@ type ('a, 'b) ml_object = {
   ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun;
   ml_subst : Mod_subst.substitution -> 'b -> 'b;
   ml_interp : environment -> 'b -> valexpr Proofview.tactic;
-  ml_print : Environ.env -> 'b -> Pp.t;
+  ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
 }
 
 val define_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object -> unit
diff --git a/user-contrib/Ltac2/tac2print.ml b/user-contrib/Ltac2/tac2print.ml
index a37fe2f7a5..fe62de1fb3 100644
--- a/user-contrib/Ltac2/tac2print.ml
+++ b/user-contrib/Ltac2/tac2print.ml
@@ -274,7 +274,9 @@ let pr_glbexpr_gen lvl c =
     paren (hov 0 (c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl)))
   | GTacExt (tag, arg) ->
     let tpe = interp_ml_object tag in
-    hov 0 (tpe.ml_print (Global.env ()) arg) (* FIXME *)
+    let env = Global.env() in
+    let sigma = Evd.from_env env in
+    hov 0 (tpe.ml_print env sigma arg) (* FIXME *)
   | GTacPrm (prm, args) ->
     let args = match args with
     | [] -> mt ()