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/prettyp.ml | |
| parent | 71563ebb86a83bc7cdfc17f58493f59428d764b0 (diff) | |
The only abstraction-breaking function in Univ is now AUContext.instance.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 7 |
1 files changed, 5 insertions, 2 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 |