diff options
Diffstat (limited to 'dev/top_printers.mli')
| -rw-r--r-- | dev/top_printers.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/top_printers.mli b/dev/top_printers.mli index dad6dcc1c..c23ba964c 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -87,7 +87,7 @@ val ppclosedglobconstr : Ltac_pretype.closed_glob_constr -> unit val ppclosedglobconstridmap : Ltac_pretype.closed_glob_constr Names.Id.Map.t -> unit -val ppglobal : Globnames.global_reference -> unit +val ppglobal : Names.GlobRef.t -> unit val ppconst : Names.KerName.t * (Constr.constr, 'a) Environ.punsafe_judgment -> unit |