diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/recordops.ml | 5 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 4 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 4 |
3 files changed, 7 insertions, 6 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 1cb694da66..9fc2573aca 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -198,7 +198,8 @@ let warn_projection_no_head_constant = let compute_canonical_projections warn (con,ind) = let env = Global.env () in let ctx = Environ.constant_context env con in - let u = Univ.UContext.instance ctx in + let u = Univ.AUContext.instance ctx in + let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in let v = (mkConstU (con,u)) in let ctx = Univ.ContextSet.of_context ctx in let c = Environ.constant_value_in env (con,u) in @@ -298,7 +299,7 @@ let error_not_structure ref = let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in let env = Global.env () in - let u = Environ.constant_instance env sp in + let u = Univ.AUContext.instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 201f79c39f..bae831b637 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -117,10 +117,10 @@ let typeclass_univ_instance (cl,u') = match cl.cl_impl with | ConstRef c -> let cb = Global.lookup_constant c in - Declareops.constant_polymorphic_instance cb + Univ.AUContext.instance (Declareops.constant_polymorphic_context cb) | IndRef c -> let mib,oib = Global.lookup_inductive c in - Declareops.inductive_polymorphic_instance mib + Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) | _ -> Univ.Instance.empty in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b3eaa3cb95..66cc42cb61 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -174,7 +174,7 @@ and nf_whd env sigma whd typ = | Vatom_stk(Aind ((mi,i) as ind), stk) -> let mib = Environ.lookup_mind mi env in let nb_univs = - Univ.Instance.length (Declareops.inductive_polymorphic_instance mib) + Univ.AUContext.size (Declareops.inductive_polymorphic_context mib) in let mk u = let pind = (ind, u) in (mkIndU pind, type_of_ind env pind) @@ -203,7 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk = | ConstKey cst -> let cbody = Environ.lookup_constant cst env in let nb_univs = - Univ.Instance.length (Declareops.constant_polymorphic_instance cbody) + Univ.AUContext.size (Declareops.constant_polymorphic_context cbody) in let mk u = let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst) |