aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--COMPATIBILITY8
-rw-r--r--kernel/closure.ml4
-rw-r--r--kernel/declarations.mli14
-rw-r--r--kernel/declareops.ml6
-rw-r--r--kernel/entries.mli7
-rw-r--r--kernel/indtypes.ml14
-rw-r--r--kernel/indtypes.mli2
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/term_typing.ml4
-rw-r--r--library/declare.ml4
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/evarconv.ml3
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/unification.ml5
-rw-r--r--printing/prettyp.ml2
-rw-r--r--theories/Classes/DecidableClass.v2
-rw-r--r--theories/Classes/RelationClasses.v2
-rw-r--r--theories/Numbers/Cyclic/Abstract/CyclicAxioms.v8
-rw-r--r--theories/Numbers/Natural/BigN/Nbasic.v4
-rw-r--r--toplevel/discharge.ml3
-rw-r--r--toplevel/record.ml36
-rw-r--r--toplevel/record.mli2
23 files changed, 65 insertions, 73 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY
index bf4e6dedde..57553f9e1a 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -24,14 +24,6 @@ Universe Polymorphism.
(e.g. induction). Extra "Transparent" might have to be added to
revert opacity of constants.
-Records, Classes.
-
-- The generated binder name of the class argument of projections
- in type class declarations is now the same as for the corresponding
- record name and is the lowercase first character of the class name.
- E.g for [Class Foo (A : Type) := foo : A -> A], foo's class argument
- has name [f].
-
Potential sources of incompatibilities between Coq V8.3 and V8.4
----------------------------------------------------------------
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 23861347a8..545325a2a9 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -871,8 +871,8 @@ let rec get_parameters depth n argstk =
let eta_expand_ind_stack env ind m s (f, s') =
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
- | Some (projs,pbs) when Array.length projs > 0
- && mib.Declarations.mind_finite <> Decl_kinds.CoFinite ->
+ | Some (Some (_,projs,pbs)) when
+ mib.Declarations.mind_finite <> Decl_kinds.CoFinite ->
(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
let pars = mib.Declarations.mind_nparams in
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 6b3f6c72f4..d908bcbe21 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -97,6 +97,15 @@ type wf_paths = recarg Rtree.t
v}
*)
+(** Record information:
+ If the record is not primitive, then None
+ Otherwise, we get:
+ - The identifier for the binder name of the record in primitive projections.
+ - The constants associated to each projection.
+ - The checked projection bodies. *)
+
+type record_body = (Id.t * constant array * projection_body array) option
+
type regular_inductive_arity = {
mind_user_arity : types;
mind_sort : sorts;
@@ -153,10 +162,7 @@ type mutual_inductive_body = {
mind_packets : one_inductive_body array; (** The component of the mutual inductive block *)
- mind_record : (constant array * projection_body array) option;
- (** Whether the inductive type has been declared as a record,
- In the case it is primitive we get its projection names and checked
- projection bodies, otherwise both arrays are empty. *)
+ mind_record : record_body option; (** The record information *)
mind_finite : Decl_kinds.recursivity_kind; (** Whether the type is inductive or coinductive *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 5b937207fd..51e435d796 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -237,14 +237,14 @@ let subst_mind_packet sub mbp =
mind_nb_args = mbp.mind_nb_args;
mind_reloc_tbl = mbp.mind_reloc_tbl }
-let subst_mind_record sub (ps, pb as r) =
+let subst_mind_record sub (id, ps, pb as r) =
let ps' = Array.smartmap (subst_constant sub) ps in
let pb' = Array.smartmap (subst_const_proj sub) pb in
if ps' == ps && pb' == pb then r
- else (ps', pb')
+ else (id, ps', pb')
let subst_mind_body sub mib =
- { mind_record = Option.smartmap (subst_mind_record sub) mib.mind_record ;
+ { mind_record = Option.smartmap (Option.smartmap (subst_mind_record sub)) mib.mind_record ;
mind_finite = mib.mind_finite ;
mind_ntypes = mib.mind_ntypes ;
mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
diff --git a/kernel/entries.mli b/kernel/entries.mli
index bf47ff90ee..f6958849b0 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -41,9 +41,10 @@ type one_inductive_entry = {
mind_entry_lc : constr list }
type mutual_inductive_entry = {
- mind_entry_record : bool option;
- (** Some true: primitive record
- Some false: non-primitive record *)
+ mind_entry_record : (Id.t option) option;
+ (** Some (Some id): primitive record with id the binder name of the record
+ in projections.
+ Some None: non-primitive record *)
mind_entry_finite : Decl_kinds.recursivity_kind;
mind_entry_params : (Id.t * local_entry) list;
mind_entry_inds : one_inductive_entry list;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 73a23ef059..39455a7d2a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -661,7 +661,7 @@ exception UndefinableExpansion
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 ((kn, _ as ind), u as indsp) n nparamargs params
+let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
mind_consnrealdecls mind_consnrealargs ctx =
let mp, dp, l = repr_mind kn in
let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
@@ -674,7 +674,7 @@ let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params
ci_pp_info = print_info }
in
let len = List.length ctx in
- let x = Name (Id.of_string (Unicode.lowercase_first_char (Id.to_string n))) in
+ let x = Name x in
let compat_body ccl i =
(* [ccl] is defined in context [params;x:rp] *)
(* [ccl'] is defined in context [params;x:rp;x:rp] *)
@@ -780,7 +780,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
let pkt = packets.(0) in
let isrecord =
match isrecord with
- | Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 ->
+ | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 ->
(** The elimination criterion ensures that all projections can be defined. *)
let u =
if p then
@@ -792,11 +792,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
(try
let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
let kns, projs =
- compute_projections indsp pkt.mind_typename nparamargs params
+ compute_projections indsp pkt.mind_typename rid nparamargs params
pkt.mind_consnrealdecls pkt.mind_consnrealargs fields
- in Some (kns, projs)
- with UndefinableExpansion -> Some ([||], [||]))
- | Some _ -> Some ([||], [||])
+ in Some (Some (rid, kns, projs))
+ with UndefinableExpansion -> Some None)
+ | Some _ -> Some None
| None -> None
in
(* Build the mutual inductive *)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 0d5b034049..a231b6cf9d 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -41,7 +41,7 @@ val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutua
val enforce_indices_matter : unit -> unit
val is_indices_matter : unit -> bool
-val compute_projections : pinductive -> Id.t ->
+val compute_projections : pinductive -> Id.t -> Id.t ->
int -> Context.rel_context -> int array -> int array ->
Context.rel_context ->
(constant array * projection_body array)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 58909ce012..a08184ed5e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -297,7 +297,7 @@ let elim_sorts (_,mip) = mip.mind_kelim
let is_private (mib,_) = mib.mind_private = Some true
let is_primitive_record (mib,_) =
match mib.mind_record with
- | Some (projs, _) when Array.length projs > 0 -> true
+ | Some (Some _) -> true
| _ -> false
let extended_rel_list n hyps =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a3c4d98490..232508bc82 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -169,11 +169,11 @@ let infer_declaration env kn dcl =
let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
let kn, pb =
match mib.mind_record with
- | Some (kns, pbs) ->
+ | Some (Some (id, kns, pbs)) ->
if i < Array.length pbs then
kns.(i), pbs.(i)
else assert false
- | None -> assert false
+ | _ -> assert false
in
let term, typ = pb.proj_eta in
Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
diff --git a/library/declare.ml b/library/declare.ml
index 8ec52d16a5..1c9e10a190 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -382,7 +382,7 @@ let inInductive : inductive_obj -> obj =
let declare_projections mind =
let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
match spec.mind_record with
- | Some (kns, pjs) ->
+ | Some (Some (_, kns, pjs)) ->
Array.iteri (fun i kn ->
let id = Label.to_id (Constant.label kn) in
let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
@@ -390,7 +390,7 @@ let declare_projections mind =
IsDefinition StructureComponent)
in
assert(eq_constant kn kn')) kns
- | None -> ()
+ | Some None | None -> ()
(* for initial declaration *)
let declare_mind isrecord mie =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index aa0232d19e..ea22396731 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -215,7 +215,7 @@ let oib_equal o1 o2 =
Array.equal Id.equal o1.mind_consnames o2.mind_consnames
let eq_record x y =
- Option.equal (fun (x, y) (x', y') -> Array.for_all2 eq_constant x x') x y
+ Option.equal (Option.equal (fun (_, x, y) (_, x', y') -> Array.for_all2 eq_constant x x')) x y
let mib_equal m1 m2 =
Array.equal oib_equal m1.mind_packets m1.mind_packets &&
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 32ac374a1e..f3f58d4371 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1307,7 +1307,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
let mk_case pb (ci,pred,c,brs) =
let mib = lookup_mind (fst ci.ci_ind) pb.env in
match mib.mind_record with
- | Some (cs, pbs) when Array.length pbs > 0 ->
+ | Some (Some (_, cs, pbs)) ->
Reduction.beta_appvect brs.(0)
(Array.map (fun p -> mkProj (Projection.make p false, c)) cs)
| _ -> mkCase (ci,pred,c,brs)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index fc726c2307..cdb38ecea3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -798,8 +798,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),
and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
- | Some (projs, pbs) when Array.length projs > 0
- && mib.Declarations.mind_finite <> Decl_kinds.CoFinite ->
+ | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite ->
let pars = mib.Declarations.mind_nparams in
(try
let l1' = Stack.tail pars sk1 in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 24bf7cbc03..91072dce8c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -334,7 +334,7 @@ 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 (projs, pbs) when Array.length projs > 0 -> Some projs
+ | Some (Some (id, projs, pbs)) -> Some projs
| _ -> None
(* substitution in a signature *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 370f3cee9c..2a6fd6fe7d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -523,8 +523,7 @@ let is_eta_constructor_app env f l1 =
| Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
let mib = lookup_mind (fst ind) env in
(match mib.Declarations.mind_record with
- | Some (exp,projs) when Array.length projs > 0
- && mib.Declarations.mind_finite <> Decl_kinds.CoFinite ->
+ | Some (Some (_, exp,projs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite ->
Array.length projs == Array.length l1 - mib.Declarations.mind_nparams
| _ -> false)
| _ -> false
@@ -534,7 +533,7 @@ let eta_constructor_app env f l1 term =
| Construct (((_, i as ind), j), u) ->
let mib = lookup_mind (fst ind) env in
(match mib.Declarations.mind_record with
- | Some (projs, _) ->
+ | Some (Some (_, projs, _)) ->
let npars = mib.Declarations.mind_nparams in
let pars, l1' = Array.chop npars l1 in
let arg = Array.append pars [|term|] in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 08d7c237d4..e0f6ef25cc 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -205,7 +205,7 @@ let print_polymorphism ref =
else "not universe polymorphic")
let print_primitive_record mipv = function
- | Some (ps,_) when Array.length ps > 0 ->
+ | Some (Some (_, ps,_)) ->
[pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion."]
| _ -> []
diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v
index 5186014e2e..b80903dc12 100644
--- a/theories/Classes/DecidableClass.v
+++ b/theories/Classes/DecidableClass.v
@@ -44,7 +44,7 @@ Qed.
(** The generic function that should be used to program, together with some
useful tactics. *)
-Definition decide P {H : Decidable P} := Decidable_witness (d:=H).
+Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H).
Ltac _decide_ P H :=
let b := fresh "b" in
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index ca4bf9cdf2..3bd9dcd12e 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -202,7 +202,7 @@ Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_insta
Hint Extern 4 (subrelation (flip _) _) =>
class_apply @subrelation_symmetric : typeclass_instances.
-Arguments irreflexivity {A R i} [x] _.
+Arguments irreflexivity {A R Irreflexive} [x] _.
Hint Resolve irreflexivity : ord.
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 4a4451078c..17c69d226f 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -93,13 +93,6 @@ Module ZnZ.
lor : t -> t -> t;
land : t -> t -> t;
lxor : t -> t -> t }.
-
- Arguments ZnZ.to_Z t Ops _ : rename.
- Arguments ZnZ.zero t Ops : rename.
- Arguments ZnZ.succ t Ops _ : rename.
- Arguments ZnZ.add_c t Ops _ _ : rename.
- Arguments ZnZ.mul_c t Ops _ _ : rename.
- Arguments ZnZ.compare t Ops _ _ : rename.
Section Specs.
Context {t : Type}{ops : Ops t}.
@@ -219,7 +212,6 @@ Module ZnZ.
End Specs.
Arguments Specs {t} ops.
- Arguments ZnZ.spec_0 t ops Specs : rename.
(** Generic construction of double words *)
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 338b5c7f94..e8a9940bd0 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -20,8 +20,8 @@ Arguments mk_zn2z_ops [t] ops.
Arguments mk_zn2z_ops_karatsuba [t] ops.
Arguments mk_zn2z_specs [t ops] specs.
Arguments mk_zn2z_specs_karatsuba [t ops] specs.
-Arguments ZnZ.digits [t] Ops : rename.
-Arguments ZnZ.zdigits [t] Ops : rename.
+Arguments ZnZ.digits [t] Ops.
+Arguments ZnZ.zdigits [t] Ops.
Lemma Pshiftl_nat_Zpower : forall n p,
Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 9de0edea81..1823e3a89a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -104,8 +104,9 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
let abs_ctx = Univ.instantiate_univ_context abs_ctx in
let univs = Univ.UContext.union abs_ctx univs in
let record = match mib.mind_record with
+ | Some (Some (id, _, _)) -> Some (Some id)
+ | Some None -> Some None
| None -> None
- | Some (_, a) -> Some (Array.length a > 0)
in
{ mind_entry_record = record;
mind_entry_finite = mib.mind_finite;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ccb6afbcc9..dfeedfbc83 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -226,7 +226,7 @@ let instantiate_possibly_recursive_type indu paramdecls fields =
Termops.substl_rel_context (subst@[mkIndU indu]) fields
(* We build projections *)
-let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
+let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let u = Inductive.inductive_instance mib in
@@ -236,15 +236,15 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
let r = mkIndU (indsp,u) in
let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in
let paramargs = Termops.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
- let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in
+ let x = Name binder_name in
let fields = instantiate_possibly_recursive_type indu paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
let primitive =
if !primitive_flag then
let is_primitive =
match mib.mind_record with
- | Some (projs, _) -> Array.length projs > 0
- | None -> false
+ | Some (Some _) -> true
+ | Some None | None -> false
in
if not is_primitive then
Flags.if_verbose msg_warning
@@ -345,6 +345,11 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity fieldim
let args = Termops.extended_rel_list nfields params in
let ind = applist (mkRel (1+nparams+nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
+ let binder_name =
+ match name with
+ | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id))
+ | Some n -> n
+ in
let mie_ind =
{ mind_entry_typename = id;
mind_entry_arity = arity;
@@ -353,7 +358,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity fieldim
in
let mie =
{ mind_entry_params = List.map degenerate_decl params;
- mind_entry_record = Some !primitive_flag;
+ mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
mind_entry_finite = finite;
mind_entry_inds = [mie_ind];
mind_entry_polymorphic = poly;
@@ -362,7 +367,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity fieldim
let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
- let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
+ let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in
let build = ConstructRef cstr in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
@@ -378,17 +383,14 @@ let implicits_of_context ctx =
1 (List.rev (Anonymous :: (List.map pi1 ctx)))
let declare_class finite def poly ctx id idbuild paramimpls params arity fieldimpls fields
- ?(kind=StructureComponent) ?name is_coe coers priorities sign =
+ ?(kind=StructureComponent) is_coe coers priorities sign =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
- (* if def then *)
- let len = List.length params in
- let impls = implicits_of_context params in
- List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
- (* else List.map (fun x -> (ExplByPos (1, None), (true, true, true)) :: *)
- (* Impargs.lift_implicits 1 x) fieldimpls *)
+ let len = List.length params in
+ let impls = implicits_of_context params in
+ List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
in
- let record_name = Id.of_string (Unicode.lowercase_first_char (Id.to_string (snd id))) in
+ let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
let impl, projs =
match fields with
| [(Name proj_name, _, field)] when def ->
@@ -402,9 +404,9 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in
let proj_type =
- it_mkProd_or_LetIn (mkProd(Name record_name, inst_type, lift 1 field)) params in
+ it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
let proj_body =
- it_mkLambda_or_LetIn (mkLambda (Name record_name, inst_type, mkRel 1)) params in
+ it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
let proj_entry = Declare.definition_entry ~types:proj_type ~poly ~univs:ctx proj_body in
let proj_cst = Declare.declare_constant proj_name
(DefinitionEntry proj_entry, IsDefinition Definition)
@@ -421,7 +423,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
| _ ->
let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
params arity fieldimpls fields
- ~kind:Method ~name:record_name false (List.map (fun _ -> false) fields) sign
+ ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
in
let coers = List.map2 (fun coe pri ->
Option.map (fun b ->
diff --git a/toplevel/record.mli b/toplevel/record.mli
index befa5f72c0..2422b45bd2 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -21,7 +21,7 @@ val primitive_flag : bool ref
as coercions accordingly to [coers]; it returns the absolute names of projections *)
val declare_projections :
- inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
+ inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
coercion_flag list -> manual_explicitation list list -> rel_context ->
(Name.t * bool) list * constant option list
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 07:33:04 +0000