aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/cic.mli2
-rw-r--r--checker/subtyping.ml2
-rw-r--r--checker/typeops.ml2
-rw-r--r--checker/values.ml4
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/indtypes.ml2
-rw-r--r--kernel/nativecode.ml5
-rw-r--r--kernel/nativelambda.ml3
-rw-r--r--kernel/typeops.ml2
-rw-r--r--plugins/extraction/extraction.ml6
-rw-r--r--pretyping/detyping.ml3
12 files changed, 16 insertions, 19 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index 3304b032e..ee7914f99 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -207,7 +207,7 @@ type inline = int option
always transparent. *)
type projection_body = {
- proj_ind : MutInd.t;
+ proj_ind : inductive;
proj_npars : int;
proj_arg : int;
proj_type : constr; (* Type under params *)
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index f4ae02084..6a051a5a9 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -126,7 +126,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
in
let eq_projection_body p1 p2 =
let check eq f = if not (eq (f p1) (f p2)) then error () in
- check MutInd.equal (fun x -> x.proj_ind);
+ check eq_ind (fun x -> x.proj_ind);
check (==) (fun x -> x.proj_npars);
check (==) (fun x -> x.proj_arg);
check (eq_constr) (fun x -> x.proj_type);
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 18f07dc0b..345ee5b8f 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -203,7 +203,7 @@ let judge_of_projection env p c ct =
try find_rectype env ct
with Not_found -> error_case_not_inductive env (c, ct)
in
- assert(MutInd.equal pb.proj_ind (fst ind));
+ assert(eq_ind pb.proj_ind ind);
let ty = subst_instance_constr u pb.proj_type in
substl (c :: List.rev args) ty
diff --git a/checker/values.ml b/checker/values.ml
index 31e65729b..c0ddc1908 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli
+MD5 2356846eddb0113e5e75bf8b46cddaee checker/cic.mli
*)
@@ -225,7 +225,7 @@ let v_cst_def =
let v_projbody =
v_tuple "projection_body"
- [|v_cst;Int;Int;v_constr|]
+ [|v_ind;Int;Int;v_constr|]
let v_typing_flags =
v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7bd7d6c9c..bb81f7514 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -50,7 +50,7 @@ type inline = int option
always transparent. *)
type projection_body = {
- proj_ind : MutInd.t;
+ proj_ind : inductive;
proj_npars : int;
proj_arg : int; (** Projection index, starting from 0 *)
proj_type : types; (* Type under params *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 1b73096f7..ad5167d8b 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -84,7 +84,7 @@ let subst_const_def sub def = match def with
| OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)
let subst_const_proj sub pb =
- { pb with proj_ind = subst_mind sub pb.proj_ind;
+ { pb with proj_ind = subst_ind sub pb.proj_ind;
proj_type = subst_mps sub pb.proj_type;
}
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 14f2a3d8f..5b3bca3a0 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -839,7 +839,7 @@ let compute_projections ((kn, _ as ind), u) nparamargs params
(* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
to [params, x:I |- t(proj1 x,..,projj x)] *)
let fterm = mkProj (Projection.make kn false, mkRel 1) in
- let body = { proj_ind = fst ind; proj_npars = nparamargs;
+ let body = { proj_ind = ind; proj_npars = nparamargs;
proj_arg = i; proj_type = projty; } in
(i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
| Anonymous -> raise UndefinableExpansion
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 8257dc8b8..914168695 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1965,6 +1965,7 @@ let compile_mind prefix ~interactive mb mind stack =
in
let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in
let add_proj j acc pb =
+ let () = assert (eq_ind ind pb.proj_ind) in
let tbl = ob.mind_reloc_tbl in
(* Building info *)
let ci = { ci_ind = ind; ci_npar = nparams;
@@ -1985,7 +1986,7 @@ let compile_mind prefix ~interactive mb mind stack =
let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in
- let gn = Gproj ("", (pb.proj_ind, j), pb.proj_arg) in
+ let gn = Gproj ("", ind, pb.proj_arg) in
Glet (gn, mkMLlam [|c_uid|] code) :: acc
in
let projs = match mb.mind_record with
@@ -2052,7 +2053,7 @@ let compile_deps env sigma prefix ~interactive init t =
| Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
| Proj (p,c) ->
let pb = lookup_projection p env in
- let init = compile_mind_deps env prefix ~interactive init pb.proj_ind in
+ let init = compile_mind_deps env prefix ~interactive init (fst pb.proj_ind) in
aux env lvl init c
| Case (ci, p, c, ac) ->
let mind = fst ci.ci_ind in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 0325a00b4..a809e1b18 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -520,8 +520,7 @@ let rec lambda_of_constr env sigma c =
| Proj (p, c) ->
let pb = lookup_projection p !global_env in
- (** FIXME: handle mutual records *)
- let ind = (pb.proj_ind, 0) in
+ let ind = pb.proj_ind in
let prefix = get_mind_prefix !global_env (fst ind) in
mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|]
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 325d5cecd..34ed2afb2 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -301,7 +301,7 @@ let type_of_projection env p c ct =
try find_rectype env ct
with Not_found -> error_case_not_inductive env (make_judge c ct)
in
- assert(MutInd.equal pb.proj_ind (fst ind));
+ assert(eq_ind pb.proj_ind ind);
let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
substl (c :: CList.rev args) ty
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 3a61c7747..bbf56525a 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1069,8 +1069,7 @@ let extract_constant env kn cb =
| false -> mk_typ (get_body c)
| true ->
let pb = lookup_projection (Projection.make kn false) env in
- (** FIXME: handle mutual records *)
- let ind = (pb.Declarations.proj_ind, 0) in
+ let ind = pb.Declarations.proj_ind in
let bodies = Inductiveops.legacy_match_projection env ind in
let body = bodies.(pb.Declarations.proj_arg) in
mk_typ (EConstr.of_constr body))
@@ -1086,8 +1085,7 @@ let extract_constant env kn cb =
| false -> mk_def (get_body c)
| true ->
let pb = lookup_projection (Projection.make kn false) env in
- (** FIXME: handle mutual records *)
- let ind = (pb.Declarations.proj_ind, 0) in
+ let ind = pb.Declarations.proj_ind in
let bodies = Inductiveops.legacy_match_projection env ind in
let body = bodies.(pb.Declarations.proj_arg) in
mk_def (EConstr.of_constr body))
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index fe49d64c7..23a985dc3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -690,8 +690,7 @@ and detype_r d flags avoid env sigma t =
let c' =
try
let pb = Environ.lookup_projection p (snd env) in
- (** FIXME: handle mutual records *)
- let ind = (pb.Declarations.proj_ind, 0) in
+ let ind = pb.Declarations.proj_ind in
let bodies = Inductiveops.legacy_match_projection (snd env) ind in
let body = bodies.(pb.Declarations.proj_arg) in
let ty = Retyping.get_type_of (snd env) sigma c in
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 09:08:07 +0000