diff options
| -rw-r--r-- | library/global.ml | 12 | ||||
| -rw-r--r-- | library/global.mli | 4 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 6 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 5 |
4 files changed, 13 insertions, 14 deletions
diff --git a/library/global.ml b/library/global.ml index e90151bff..cb6334c74 100644 --- a/library/global.ml +++ b/library/global.ml @@ -194,26 +194,24 @@ let type_of_global_unsafe r = let type_of_global_in_context env r = match r with - | VarRef id -> Environ.named_type id env, Univ.UContext.empty + | VarRef id -> Environ.named_type id env, Univ.AUContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in let univs = Declareops.constant_polymorphic_context cb in - let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in Typeops.type_of_constant_type env cb.Declarations.const_type, univs | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + let inst = Univ.make_abstract_instance univs in + let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in Inductive.type_of_inductive env (specif, inst), univs | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + let inst = Univ.make_abstract_instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs let universes_of_global env r = diff --git a/library/global.mli b/library/global.mli index 5ddf54b4a..d9190736f 100644 --- a/library/global.mli +++ b/library/global.mli @@ -123,8 +123,8 @@ val is_template_polymorphic : Globnames.global_reference -> bool val is_type_in_type : Globnames.global_reference -> bool val type_of_global_in_context : Environ.env -> - Globnames.global_reference -> Constr.types Univ.in_universe_context -(** Returns the type of the constant in its global or local universe + Globnames.global_reference -> Constr.types * Univ.AUContext.t +(** Returns the type of the constant in its local universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter. *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index bae831b63..6de5bc28b 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -279,8 +279,10 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in let ty, ctx = Global.type_of_global_in_context env glob in + let inst, ctx = Universes.fresh_instance_from ctx None in + let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in - let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let rec aux pri c ty path = match class_of_constr sigma ty with | None -> [] @@ -317,7 +319,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in + let term = Universes.constr_of_global_univ (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 6d93f0e41..3d97a767c 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -383,9 +383,8 @@ let do_mutual_induction_scheme lnamedepindsort = match inst with | None -> let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in - let ctxs = Univ.ContextSet.of_context ctx in - let evd = Evd.from_ctx (Evd.evar_universe_context_of ctxs) in - let u = Univ.UContext.instance ctx in + let u, ctx = Universes.fresh_instance_from ctx None in + let evd = Evd.from_ctx (Evd.evar_universe_context_of ctx) in evd, (ind,u), Some u | Some ui -> evd, (ind, ui), inst in |