diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-12 15:29:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | 34bcd562cc9c8e5e6b0f3b79a15b9c55dd98813e (patch) | |
| tree | 461be63f369d2018ef427ae682cd152dc6bccbec /printing | |
| parent | 71563ebb86a83bc7cdfc17f58493f59428d764b0 (diff) | |
The only abstraction-breaking function in Univ is now AUContext.instance.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 7 | ||||
| -rw-r--r-- | printing/printmod.ml | 15 |
2 files changed, 18 insertions, 4 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index a0c88a7af..5cd79ed6d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -532,7 +532,9 @@ let print_constant with_values sep sp = begin match cb.const_universes with | Monomorphic_const ctx -> ctx - | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + | Polymorphic_const ctx -> + let inst = Univ.AUContext.instance ctx in + Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) end | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in @@ -542,7 +544,8 @@ let print_constant with_values sep sp = Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) | Polymorphic_const ctx -> assert(Univ.ContextSet.is_empty body_uctxs); - Univ.instantiate_univ_context ctx + let inst = Univ.AUContext.instance ctx in + Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) in let ctx = Evd.evar_universe_context_of_binders diff --git a/printing/printmod.ml b/printing/printmod.ml index 2e0e6d284..5c7dcdc10 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -110,6 +110,17 @@ let print_one_inductive env sigma mib ((_,i) as ind) = str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes +let instantiate_cumulativity_info cumi = + let open Univ in + let univs = ACumulativityInfo.univ_context cumi in + let subtyp = ACumulativityInfo.subtyp_context cumi in + let expose ctx = + let inst = AUContext.instance ctx in + let cst = AUContext.instantiate inst ctx in + UContext.make (inst, cst) + in + CumulativityInfo.make (expose univs, expose subtyp) + let print_mutual_inductive env mind mib = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in @@ -133,7 +144,7 @@ let print_mutual_inductive env mind mib = | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> Printer.pr_cumulativity_info - sigma (Univ.instantiate_cumulativity_info cumi)) + sigma (instantiate_cumulativity_info cumi)) let get_fields = let rec prodec_rec l subst c = @@ -191,7 +202,7 @@ let print_record env mind mib = | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> Printer.pr_cumulativity_info - sigma (Univ.instantiate_cumulativity_info cumi) + sigma (instantiate_cumulativity_info cumi) ) let pr_mutual_inductive_body env mind mib = |