diff options
Diffstat (limited to 'ltac/pptactic.mli')
| -rw-r--r-- | ltac/pptactic.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/pptactic.mli b/ltac/pptactic.mli index 86e3ea548..5fff3062d 100644 --- a/ltac/pptactic.mli +++ b/ltac/pptactic.mli @@ -34,8 +34,8 @@ type 'a glob_extra_genarg_printer = 'a -> std_ppcmds type 'a extra_genarg_printer = - (Term.constr -> std_ppcmds) -> - (Term.constr -> std_ppcmds) -> + (EConstr.constr -> std_ppcmds) -> + (EConstr.constr -> std_ppcmds) -> (tolerability -> Val.t -> std_ppcmds) -> 'a -> std_ppcmds |