diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-29 23:48:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:44 +0100 |
| commit | 27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 (patch) | |
| tree | 7f69b79408e4433227d59655d78342108bfed540 /pretyping | |
| parent | 390fd4ac0a969103caeb5db3e5138e26f9a533de (diff) | |
Moving printing code from Evd to Termops.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index d4e156fa4..c8d945c0b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -422,7 +422,7 @@ let detype_sort sigma = function | Type u -> GType (if !print_universes - then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)] + then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)] else []) type binder_kind = BProd | BLambda | BLetIn @@ -434,7 +434,7 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - GType (Some (dl, Pp.string_of_ppcmds (Evd.pr_evd_level sigma l))) + GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l))) let detype_instance sigma l = if Univ.Instance.is_empty l then None @@ -533,7 +533,7 @@ let rec detype flags avoid env sigma t = let id,l = try let id = match Evd.evar_ident evk sigma with - | None -> Evd.pr_evar_suggested_name evk sigma + | None -> Termops.pr_evar_suggested_name evk sigma | Some id -> id in let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in |