diff options
| author | coqbot-app[bot] | 2020-11-26 11:06:00 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-26 11:06:00 +0000 |
| commit | 0fc82e9651ee1dbc429c9b328b90ad8ad1a3cb14 (patch) | |
| tree | c99091031ad585bf3249ae089e12f44d4e5d83ce /printing/printer.mli | |
| parent | 5c7f71a270b265d1ae3f86cb2a29d28f2310edc5 (diff) | |
| parent | 4011a9137fdebe16aa40cb03ba5ce32c09687c69 (diff) | |
Merge PR #13415: Separate interning and pretyping of universes
Reviewed-by: mattam82
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index ea388ae57e..732af5570d 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -107,9 +107,9 @@ val pr_closed_glob_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t -val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_lglob_constr_env : env -> evar_map -> 'a glob_constr_g -> Pp.t -val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_glob_constr_env : env -> evar_map -> 'a glob_constr_g -> Pp.t val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t |