diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-17 20:17:17 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-17 20:17:17 +0530 |
| commit | 3bcca0aecb368a723d247d1f8b2348790bc87035 (patch) | |
| tree | 81dbfb0613e67109887e9121e3d984bf752aa4ab /printing | |
| parent | 014878c3a05365d4af7e3edcfc8d612c45fdf1f3 (diff) | |
Univs: proper printing of global and local universe names (only
printing functions touched in the kernel).
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 2 | ||||
| -rw-r--r-- | printing/printer.ml | 12 | ||||
| -rw-r--r-- | printing/printer.mli | 3 |
3 files changed, 6 insertions, 11 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7cc193a8d..f8264e5af 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1451,7 +1451,7 @@ let () = (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id))) ; Genprint.register_print0 Constrarg.wit_sort - pr_glob_sort pr_glob_sort pr_sort; + pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 Constrarg.wit_uconstr Ppconstr.pr_constr_expr diff --git a/printing/printer.ml b/printing/printer.ml index 7d5b71f34..3403fb9c3 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -143,17 +143,12 @@ let pr_constr_pattern t = let (sigma, env) = get_current_context () in pr_constr_pattern_env env sigma t -let pr_sort s = pr_glob_sort (extern_sort s) +let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let _ = Termops.set_print_constr (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t)) let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" -let pr_univ_cstr (c:Univ.constraints) = - if !Detyping.print_universes && not (Univ.Constraint.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 (Univ.pr_constraints c)) c - else - mt() (** Term printers resilient to [Nametab] errors *) @@ -216,7 +211,8 @@ let safe_pr_constr t = let pr_universe_ctx c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 (Univ.pr_universe_context c)) c + fnl()++pr_in_comment (fun c -> v 0 + (Univ.pr_universe_context Universes.pr_with_global_universes c)) c else mt() @@ -229,7 +225,7 @@ let pr_global = pr_global_env Id.Set.empty let pr_puniverses f env (c,u) = f env c ++ (if !Constrextern.print_universes then - str"(*" ++ Univ.Instance.pr u ++ str"*)" + str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" else mt ()) let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) diff --git a/printing/printer.mli b/printing/printer.mli index 75ab1722d..6b9c70815 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -79,12 +79,11 @@ val pr_constr_pattern : constr_pattern -> std_ppcmds val pr_cases_pattern : cases_pattern -> std_ppcmds -val pr_sort : sorts -> std_ppcmds +val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds -val pr_univ_cstr : Univ.constraints -> std_ppcmds val pr_universe_ctx : Univ.universe_context -> std_ppcmds (** Printing global references using names as short as possible *) |