aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evarconv.ml9
-rw-r--r--pretyping/recordops.ml22
-rw-r--r--pretyping/reductionops.ml14
-rw-r--r--pretyping/typeclasses.ml4
-rw-r--r--pretyping/vnorm.ml4
5 files changed, 26 insertions, 27 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b5d195873c..87f29ba492 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -353,9 +353,8 @@ let exact_ise_stack2 env evd f sk1 sk2 =
let check_leq_inductives evd cumi u u' =
let u = EConstr.EInstance.kind evd u in
let u' = EConstr.EInstance.kind evd u' in
- let length_ind_instance =
- Univ.Instance.length
- (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+ let length_ind_instance =
+ Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
in
let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in
if not ((length_ind_instance = Univ.Instance.length u) &&
@@ -364,9 +363,7 @@ let check_leq_inductives evd cumi u u' =
else
begin
let comp_subst = (Univ.Instance.append u u') in
- let comp_cst =
- Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst)
- in
+ let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in
Evd.add_constraints evd comp_cst
end
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 1cb694da66..c498089ca8 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -189,22 +189,28 @@ let cs_pattern_of_constr t =
let warn_projection_no_head_constant =
CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
- (fun (t,con_pp,proji_sp_pp) ->
+ (fun (sign,env,t,con,proji_sp) ->
+ let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
+ let env = Termops.push_rels_assum sign env in
+ let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
+ let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
+ let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in
strbrk "Projection value has no head constant: "
- ++ Termops.print_constr (EConstr.of_constr t) ++ strbrk " in canonical instance "
+ ++ term_pp ++ strbrk " in canonical instance "
++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
(* Intended to always succeed *)
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
- let lt,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
+ let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
let t = EConstr.Unsafe.to_constr t in
- let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) lt in
+ let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in
let args = snd (decompose_app t) in
let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
lookup_structure ind in
@@ -221,9 +227,7 @@ let compute_canonical_projections warn (con,ind) =
let patt, n , args = cs_pattern_of_constr t in
((ConstRef proji_sp, patt, t, n, args) :: l)
with Not_found ->
- let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
- and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
- if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp);
+ if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp);
l
end
| _ -> l)
@@ -298,7 +302,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/reductionops.ml b/pretyping/reductionops.ml
index cc1709f1c2..21ed8e0a23 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1362,25 +1362,23 @@ let sigma_compare_instances ~flex i0 i1 sigma =
raise Reduction.NotConvertible
let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
- let ind_instance =
- Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind)
+ let len_instance =
+ Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind)
in
let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in
- if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
- (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+ if not ((len_instance = Univ.Instance.length u) &&
+ (len_instance = Univ.Instance.length u')) then
anomaly (Pp.str "Invalid inductive subtyping encountered!")
else
let comp_cst =
let comp_subst = (Univ.Instance.append u u') in
- Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbctx)
+ Univ.AUContext.instantiate comp_subst ind_sbctx
in
let comp_cst =
match cv_pb with
Reduction.CONV ->
let comp_subst = (Univ.Instance.append u' u) in
- let comp_cst' =
- Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx)
- in
+ let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in
Univ.Constraint.union comp_cst comp_cst'
| Reduction.CUMUL -> comp_cst
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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 06:55:37 +0000