diff options
| author | Matthieu Sozeau | 2015-10-28 12:36:20 -0400 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-28 12:42:00 -0400 |
| commit | 0132b5b51fc1856356fb74130d3dea7fd378f76c (patch) | |
| tree | da5c0ec53dcecafb2fab5db1a112fac8b6311e60 /printing/printer.ml | |
| parent | 89be9efbf6dbd8a04fb8ccab4c9aa7a11b9a0f03 (diff) | |
Univs: local names handling.
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index f4852b1089..202b4f2bc7 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -208,10 +208,10 @@ let safe_pr_constr t = let (sigma, env) = get_current_context () in safe_pr_constr_env env sigma t -let pr_universe_ctx c = +let pr_universe_ctx sigma c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context Universes.pr_with_global_universes c)) c + (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c else mt() @@ -825,7 +825,7 @@ let pr_polymorphic b = if b then str"Polymorphic " else str"Monomorphic " else mt () -let pr_universe_instance ctx = +let pr_universe_instance evd ctx = let inst = Univ.UContext.instance ctx in - str"@{" ++ Univ.Instance.pr Univ.Level.pr inst ++ str"}" + str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}" |