diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2env.ml')
| -rw-r--r-- | user-contrib/Ltac2/tac2env.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 = |