aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/detyping.mli4
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/geninterp.mli4
-rw-r--r--pretyping/glob_ops.ml8
-rw-r--r--pretyping/glob_term.ml4
-rw-r--r--pretyping/indrec.ml8
-rw-r--r--pretyping/indrec.mli3
-rw-r--r--pretyping/inductiveops.ml134
-rw-r--r--pretyping/inductiveops.mli12
-rw-r--r--pretyping/nativenorm.ml7
-rw-r--r--pretyping/pretyping.ml59
-rw-r--r--pretyping/unification.ml10
14 files changed, 197 insertions, 68 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0dd3c5944..93ca9dc5e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1425,7 +1425,7 @@ and match_current pb (initial,tomatch) =
let ci = make_case_info pb.env (fst mind) pb.casestyle in
let pred = nf_betaiota pb.env !(pb.evdref) pred in
let case =
- make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
+ make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
in
let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in
Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index df89d9eac..23a985dc3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -87,7 +87,7 @@ let encode_tuple ({CAst.loc} as r) =
module PrintingInductiveMake =
functor (Test : sig
- val encode : reference -> inductive
+ val encode : qualid -> inductive
val member_message : Pp.t -> bool -> Pp.t
val field : string
val title : string
@@ -690,7 +690,9 @@ and detype_r d flags avoid env sigma t =
let c' =
try
let pb = Environ.lookup_projection p (snd env) in
- let body = pb.Declarations.proj_body 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
let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
let body' = strip_lam_assum body in
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 5310455fe..8695d52b1 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -87,7 +87,7 @@ val subst_genarg_hook :
module PrintingInductiveMake :
functor (Test : sig
- val encode : Libnames.reference -> Names.inductive
+ val encode : Libnames.qualid -> Names.inductive
val member_message : Pp.t -> bool -> Pp.t
val field : string
val title : string
@@ -95,7 +95,7 @@ module PrintingInductiveMake :
sig
type t = Names.inductive
val compare : t -> t -> int
- val encode : Libnames.reference -> Names.inductive
+ val encode : Libnames.qualid -> Names.inductive
val subst : substitution -> t -> t
val printer : t -> Pp.t
val key : Goptions.option_name
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 520be199e..a71ef6508 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -984,9 +984,11 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
else UnifFailure(evd,(*dummy*)NotSameHead)
and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
+ let open Declarations in
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
- | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite ->
+ | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite ->
+ let (_, projs, _) = info.(snd ind) in
let pars = mib.Declarations.mind_nparams in
(try
let l1' = Stack.tail pars sk1 in
diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli
index fa522e9c3..606a6ebea 100644
--- a/pretyping/geninterp.mli
+++ b/pretyping/geninterp.mli
@@ -42,8 +42,8 @@ sig
end
-module ValTMap (M : Dyn.TParam) :
- Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ
+module ValTMap (Value : Dyn.ValueS) :
+ Dyn.MapS with type 'a key = 'a Val.typ and type 'a value = 'a Value.t
(** Dynamic types for toplevel values. While the generic types permit to relate
objects at various levels of interpretation, toplevel values are wearing
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 8ecec30cf..ba193da60 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -51,7 +51,7 @@ let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
| GProp, GProp -> true
| GSet, GSet -> true
| GType l1, GType l2 ->
- List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
+ List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2
| _ -> false
let binding_kind_eq bk1 bk2 = match bk1, bk2 with
@@ -414,8 +414,10 @@ let loc_of_glob_constr c = c.CAst.loc
(**********************************************************************)
(* Alpha-renaming *)
+exception UnsoundRenaming
+
let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l
-let test_id l id = if collide_id l id then raise Not_found
+let test_id l id = if collide_id l id then raise UnsoundRenaming
let test_na l na = Name.iter (test_id l) na
let update_subst na l =
@@ -429,8 +431,6 @@ let update_subst na l =
else na,l)
na (na,l)
-exception UnsoundRenaming
-
let rename_var l id =
try
let id' = Id.List.assoc id l in
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 54fa5328f..86245d479 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -33,11 +33,11 @@ type 'a universe_kind =
| UUnknown
| UNamed of 'a
-type level_info = Libnames.reference universe_kind
+type level_info = Libnames.qualid universe_kind
type glob_level = level_info glob_sort_gen
type glob_constraint = glob_level * Univ.constraint_type * glob_level
-type sort_info = (Libnames.reference * int) option list
+type sort_info = (Libnames.qualid * int) option list
type glob_sort = sort_info glob_sort_gen
(** Casts *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 27b029aad..4ab932723 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -304,7 +304,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
process_constr env 0 f (List.rev cstr.cs_args, recargs)
(* Main function *)
-let mis_make_indrec env sigma listdepkind mib u =
+let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
let nparams = mib.mind_nparams in
let nparrec = mib.mind_nparams_rec in
let evdref = ref sigma in
@@ -469,7 +469,7 @@ let mis_make_indrec env sigma listdepkind mib u =
(* Body on make_one_rec *)
let ((indi,u),mibi,mipi,dep,kind) = List.nth listdepkind p in
- if (mis_is_recursive_subset
+ if force_mutual || (mis_is_recursive_subset
(List.map (fun ((indi,u),_,_,_,_) -> snd indi) listdepkind)
mipi.mind_recargs)
then
@@ -558,7 +558,7 @@ let check_arities env listdepkind =
[] listdepkind
in true
-let build_mutual_induction_scheme env sigma = function
+let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function
| ((mind,u),dep,s)::lrecspec ->
let (mib,mip) = lookup_mind_specif env mind in
if dep && not (Inductiveops.has_dependent_elim mib) then
@@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function
lrecspec)
in
let _ = check_arities env listdepkind in
- mis_make_indrec env sigma listdepkind mib u
+ mis_make_indrec env sigma ~force_mutual listdepkind mib u
| _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.")
let build_induction_scheme env sigma pind dep kind =
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index d87a19d28..de9d3a0ab 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -47,7 +47,8 @@ val build_induction_scheme : env -> evar_map -> pinductive ->
(** Builds mutual (recursive) induction schemes *)
val build_mutual_induction_scheme :
- env -> evar_map -> (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list
+ env -> evar_map -> ?force_mutual:bool ->
+ (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list
(** Scheme combinators *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b1ab2d2b7..d599afe69 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -277,8 +277,8 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
let has_dependent_elim mib =
match mib.mind_record with
- | Some (Some _) -> mib.mind_finite == BiFinite
- | _ -> true
+ | PrimRecord _ -> mib.mind_finite == BiFinite
+ | NotRecord | FakeRecord -> true
(* Annotation for cases *)
let make_case_info env ind style =
@@ -346,8 +346,10 @@ let get_constructors env (ind,params) =
let get_projections env (ind,params) =
let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
match mib.mind_record with
- | Some (Some (id, projs, pbs)) -> Some projs
- | _ -> None
+ | PrimRecord infos ->
+ let (_, projs, _) = infos.(snd (fst ind)) in
+ Some projs
+ | NotRecord | FakeRecord -> None
let make_case_or_project env sigma indf ci pred c branches =
let open EConstr in
@@ -356,8 +358,8 @@ let make_case_or_project env sigma indf ci pred c branches =
| None -> (mkCase (ci, pred, c, branches))
| Some ps ->
assert(Array.length branches == 1);
+ let na, ty, t = destLambda sigma pred in
let () =
- let _, _, t = destLambda sigma pred in
let (ind, _), _ = dest_ind_family indf in
let mib, _ = Inductive.lookup_mind_specif env ind in
if (* dependent *) not (Vars.noccurn sigma 1 t) &&
@@ -368,16 +370,18 @@ let make_case_or_project env sigma indf ci pred c branches =
in
let branch = branches.(0) in
let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
- let n, subst =
+ let n, len, ctx =
List.fold_right
- (fun decl (i, subst) ->
+ (fun decl (i, j, ctx) ->
match decl with
- | LocalAssum (na, t) ->
- let t = mkProj (Projection.make ps.(i) true, c) in
- (i + 1, t :: subst)
- | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
- ctx (0, [])
- in Vars.substl subst br
+ | LocalAssum (na, ty) ->
+ let t = mkProj (Projection.make ps.(i) true, mkRel j) in
+ (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx)
+ | LocalDef (na, b, ty) ->
+ (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx))
+ ctx (0, 1, [])
+ in
+ mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx)
(* substitution in a signature *)
@@ -454,6 +458,110 @@ let build_branch_type env sigma dep p cs =
(**************************************************)
+(** From a rel context describing the constructor arguments,
+ build an expansion function.
+ The term built is expecting to be substituted first by
+ a substitution of the form [params, x : ind params] *)
+let compute_projections env (kn, i as ind) =
+ let open Term in
+ let mib = Environ.lookup_mind kn env in
+ let indu = match mib.mind_universes with
+ | Monomorphic_ind _ -> mkInd ind
+ | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx)
+ | Cumulative_ind ctx ->
+ mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx))
+ in
+ let x = match mib.mind_record with
+ | NotRecord | FakeRecord ->
+ anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+ | PrimRecord info-> Name (pi1 (info.(i)))
+ in
+ (** FIXME: handle mutual records *)
+ let pkt = mib.mind_packets.(0) in
+ let { mind_consnrealargs; mind_consnrealdecls } = pkt in
+ let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
+ let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in
+ let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
+ let mp, dp, l = MutInd.repr3 kn in
+ (** We build a substitution smashing the lets in the record parameters so
+ that typechecking projections requires just a substitution and not
+ matching with a parameter context. *)
+ let indty =
+ (* [ty] = [Ind inst] is typed in context [params] *)
+ let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
+ let ty = mkApp (indu, inst) in
+ (* [Ind inst] is typed in context [params-wo-let] *)
+ ty
+ in
+ let ci =
+ let print_info =
+ { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+ { ci_ind = ind;
+ ci_npar = nparamargs;
+ ci_cstr_ndecls = mind_consnrealdecls;
+ ci_cstr_nargs = mind_consnrealargs;
+ ci_pp_info = print_info }
+ in
+ let len = List.length ctx in
+ let compat_body ccl i =
+ (* [ccl] is defined in context [params;x:indty] *)
+ (* [ccl'] is defined in context [params;x:indty;x:indty] *)
+ let ccl' = liftn 1 2 ccl in
+ let p = mkLambda (x, lift 1 indty, ccl') in
+ let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
+ let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
+ it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
+ in
+ let projections decl (j, pbs, subst) =
+ match decl with
+ | LocalDef (na,c,t) ->
+ (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
+ to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
+ let c = liftn 1 j c in
+ (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
+ to [params, x:I |- c(params,proj1 x,..,projj x)] *)
+ let c1 = substl subst c in
+ (* From [params, x:I |- subst:field1,..,fieldj]
+ to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
+ is represented with instance of field1 last *)
+ let subst = c1 :: subst in
+ (j+1, pbs, subst)
+ | LocalAssum (na,t) ->
+ match na with
+ | Name id ->
+ let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+ (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)]
+ to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *)
+ let t = liftn 1 j t in
+ (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)]
+ to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *)
+ (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
+ to [params, x:I |- t(proj1 x,..,projj x)] *)
+ let ty = substl subst t in
+ let term = mkProj (Projection.make kn true, mkRel 1) in
+ let fterm = mkProj (Projection.make kn false, mkRel 1) in
+ let compat = compat_body ty (j - 1) in
+ let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
+ let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
+ let body = (etab, etat, compat) in
+ (j + 1, body :: pbs, fterm :: subst)
+ | Anonymous ->
+ anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+ in
+ let (_, pbs, subst) =
+ List.fold_right projections ctx (1, [], [])
+ in
+ Array.rev_of_list pbs
+
+let legacy_match_projection env ind =
+ Array.map pi3 (compute_projections env ind)
+
+let compute_projections ind mib =
+ let ans = compute_projections ind mib in
+ Array.map (fun (prj, ty, _) -> (prj, ty)) ans
+
+(**************************************************)
+
let extract_mrectype sigma t =
let open EConstr in
let (t, l) = decompose_app sigma t in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index b0d714b03..aa53f7e67 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -194,6 +194,18 @@ val make_case_or_project :
val make_default_case_info : env -> case_style -> inductive -> case_info
i*)
+val compute_projections : Environ.env -> inductive -> (constr * types) array
+(** Given a primitive record type, for every field computes the eta-expanded
+ projection and its type. *)
+
+val legacy_match_projection : Environ.env -> inductive -> constr array
+(** Given a record type, computes the legacy match-based projection of the
+ projections.
+
+ BEWARE: such terms are ill-typed, and should thus only be used in upper
+ layers. The kernel will probably badly fail if presented with one of
+ those. *)
+
(********************)
val type_of_inductive_knowing_conclusion :
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 4b8e0e096..7319846fb 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -188,12 +188,13 @@ let branch_of_switch lvl ans bs =
bs ci in
Array.init (Array.length tbl) branch
-let get_proj env ((mind, _n), i) =
+let get_proj env ((mind, n), i) =
let mib = Environ.lookup_mind mind env in
match mib.mind_record with
- | None | Some None ->
+ | NotRecord | FakeRecord ->
CErrors.anomaly (Pp.strbrk "Return type is not a primitive record")
- | Some (Some (_, projs, _)) ->
+ | PrimRecord info ->
+ let _, projs, _ = info.(n) in
Projection.make projs.(i) true
let rec nf_val env sigma v typ =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9e024b1c2..57c4d363b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -171,38 +171,37 @@ let _ =
(** Miscellaneous interpretation functions *)
-let interp_known_universe_level evd r =
- let qid = Libnames.qualid_of_reference r in
+let interp_known_universe_level evd qid =
try
- match r.CAst.v with
- | Libnames.Ident id -> Evd.universe_of_name evd id
- | Libnames.Qualid _ -> raise Not_found
+ let open Libnames in
+ if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
+ else raise Not_found
with Not_found ->
- let univ, k = Nametab.locate_universe qid.CAst.v in
+ let univ, k = Nametab.locate_universe qid in
Univ.Level.make univ k
-let interp_universe_level_name ~anon_rigidity evd r =
- try evd, interp_known_universe_level evd r
+let interp_universe_level_name ~anon_rigidity evd qid =
+ try evd, interp_known_universe_level evd qid
with Not_found ->
- match r with (* Qualified generated name *)
- | {CAst.loc; v=Libnames.Qualid qid} ->
- let dp, i = Libnames.repr_qualid qid in
- let num =
- try int_of_string (Id.to_string i)
- with Failure _ ->
- user_err ?loc ~hdr:"interp_universe_level_name"
- (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r))
- in
- let level = Univ.Level.make dp num in
- let evd =
- try Evd.add_global_univ evd level
- with UGraph.AlreadyDeclared -> evd
- in evd, level
- | {CAst.loc; v=Libnames.Ident id} -> (* Undeclared *)
- if not (is_strict_universe_declarations ()) then
- new_univ_level_variable ?loc ~name:id univ_rigid evd
- else user_err ?loc ~hdr:"interp_universe_level_name"
- (Pp.(str "Undeclared universe: " ++ Id.print id))
+ if Libnames.qualid_is_ident qid then (* Undeclared *)
+ let id = Libnames.qualid_basename qid in
+ if not (is_strict_universe_declarations ()) then
+ new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd
+ else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
+ (Pp.(str "Undeclared universe: " ++ Id.print id))
+ else
+ let dp, i = Libnames.repr_qualid qid in
+ let num =
+ try int_of_string (Id.to_string i)
+ with Failure _ ->
+ user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
+ (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
+ in
+ let level = Univ.Level.make dp num in
+ let evd =
+ try Evd.add_global_univ evd level
+ with UGraph.AlreadyDeclared -> evd
+ in evd, level
let interp_universe ?loc evd = function
| [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
@@ -232,10 +231,10 @@ let interp_known_level_info ?loc evd = function
| UUnknown | UAnonymous ->
user_err ?loc ~hdr:"interp_known_level_info"
(str "Anonymous universes not allowed here.")
- | UNamed ref ->
- try interp_known_universe_level evd ref
+ | UNamed qid ->
+ try interp_known_universe_level evd qid
with Not_found ->
- user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref)
+ user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
let interp_level_info ?loc evd : level_info -> _ = function
| UUnknown -> new_univ_level_variable ?loc univ_rigid evd
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5cf6e4b26..4ba5d2794 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -656,10 +656,12 @@ let rec is_neutral env sigma ts t =
let is_eta_constructor_app env sigma ts f l1 term =
match EConstr.kind sigma f with
- | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
+ | Construct (((_, i as ind), j), u) when j == 1 ->
+ let open Declarations in
let mib = lookup_mind (fst ind) env in
(match mib.Declarations.mind_record with
- | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite &&
+ | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite &&
+ let (_, projs, _) = info.(i) in
Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
(** Check that the other term is neutral *)
is_neutral env sigma ts term
@@ -667,11 +669,13 @@ let is_eta_constructor_app env sigma ts f l1 term =
| _ -> false
let eta_constructor_app env sigma f l1 term =
+ let open Declarations in
match EConstr.kind sigma f with
| Construct (((_, i as ind), j), u) ->
let mib = lookup_mind (fst ind) env in
(match mib.Declarations.mind_record with
- | Some (Some (_, projs, _)) ->
+ | PrimRecord info ->
+ let (_, projs, _) = info.(i) in
let npars = mib.Declarations.mind_nparams in
let pars, l1' = Array.chop npars l1 in
let arg = Array.append pars [|term|] in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-25 19:18:53 +0000