aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh9
-rw-r--r--interp/constrintern.ml8
-rw-r--r--interp/constrintern.mli4
-rw-r--r--interp/impargs.ml89
-rw-r--r--interp/impargs.mli10
-rw-r--r--interp/implicit_quantifiers.ml27
-rw-r--r--vernac/classes.ml3
-rw-r--r--vernac/comAssumption.ml4
-rw-r--r--vernac/comDefinition.ml25
-rw-r--r--vernac/comFixpoint.ml2
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/comInductive.ml14
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/lemmas.mli2
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/obligations.mli5
-rw-r--r--vernac/record.ml14
17 files changed, 72 insertions, 150 deletions
diff --git a/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh b/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh
new file mode 100644
index 0000000000..c8cf85e73e
--- /dev/null
+++ b/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10231" ] || [ "$CI_BRANCH" = "master+locating-warning-different-implicit-term-type" ]; then
+
+ equations_CI_REF=master+fix-manual-implicit-pr10231
+ equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+ mtac2_CI_REF=master+fix-manual-implicit-pr10231
+ mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
+
+fi
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1a81dc41a1..e55f66e856 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2435,10 +2435,8 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
let r = Retyping.relevance_of_type env sigma t in
let d = LocalAssum (make_annot na r,t) in
let impls =
- if k == Implicit then
- let na = match na with Name n -> Some n | Anonymous -> None in
- (ExplByPos (n, na), (true, true, true)) :: impls
- else impls
+ if k == Implicit then CAst.make (Some (na,true)) :: impls
+ else CAst.make None :: impls
in
(push_rel d env, sigma, d::params, succ n, impls)
| Some b ->
@@ -2447,7 +2445,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
let d = LocalDef (make_annot na r, c, t) in
(push_rel d env, sigma, d::params, n, impls))
(env,sigma,[],k+1,[]) (List.rev bl)
- in sigma, ((env, par), impls)
+ in sigma, ((env, par), List.rev impls)
let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
let int_env,bl = intern_context global_level env impl_env params in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0d4bc91f57..4bf8ee9429 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -61,10 +61,10 @@ type internalization_env = var_internalization_data Id.Map.t
val empty_internalization_env : internalization_env
val compute_internalization_data : env -> evar_map -> var_internalization_type ->
- types -> Impargs.manual_explicitation list -> var_internalization_data
+ types -> Impargs.manual_implicits -> var_internalization_data
val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type ->
- Id.t list -> types list -> Impargs.manual_explicitation list list ->
+ Id.t list -> types list -> Impargs.manual_implicits list ->
internalization_env
type ltac_sign = {
diff --git a/interp/impargs.ml b/interp/impargs.ml
index f3cdd64633..112862da18 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,7 +20,6 @@ open Lib
open Libobject
open EConstr
open Reductionops
-open Constrexpr
open Namegen
module NamedDecl = Context.Named.Declaration
@@ -341,77 +340,30 @@ let rec prepare_implicits f = function
Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
| _::imps -> None :: prepare_implicits f imps
-(*
-If found, returns Some (x,(b,fi,fo)) and l with the entry removed,
-otherwise returns None and l unchanged.
- *)
-let assoc_by_pos k l =
- let rec aux = function
- (ExplByPos (k', x), b) :: tl when Int.equal k k' -> Some (x,b), tl
- | hd :: tl -> let (x, tl) = aux tl in x, hd :: tl
- | [] -> raise Not_found
- in try aux l with Not_found -> None, l
-
-let check_correct_manual_implicits autoimps l =
- List.iter (function
- | ExplByName id,(b,fi,forced) ->
- if not forced then
- user_err
- (str "Wrong or non-dependent implicit argument name: " ++ Id.print id ++ str ".")
- | ExplByPos (i,_id),_t ->
- if i<1 || i>List.length autoimps then
- user_err
- (str "Bad implicit argument number: " ++ int i ++ str ".")
- else
- user_err
- (str "Cannot set implicit argument number " ++ int i ++
- str ": it has no name.")) l
-
-(* Take a list l of explicitations, and map them to positions. *)
-let flatten_explicitations l autoimps =
- let rec aux k l = function
- | (Name id,_)::imps ->
- let value, l' =
- try
- let eq = Constrexpr_ops.explicitation_eq in
- let flags = List.assoc_f eq (ExplByName id) l in
- Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l
- with Not_found -> assoc_by_pos k l
- in value :: aux (k+1) l' imps
- | (Anonymous,_)::imps ->
- let value, l' = assoc_by_pos k l
- in value :: aux (k+1) l' imps
- | [] when List.is_empty l -> []
- | [] ->
- check_correct_manual_implicits autoimps l;
- []
- in aux 1 l autoimps
-
let set_manual_implicits flags enriching autoimps l =
- if not (List.distinct l) then
- user_err Pp.(str "Some parameters are referred more than once.");
(* Compare with automatic implicits to recover printing data and names *)
let rec merge k autoimps explimps = match autoimps, explimps with
| autoimp::autoimps, explimp::explimps ->
let imps' = merge (k+1) autoimps explimps in
- begin match autoimp, explimp with
- | (Name id,_), Some (_, (b, fi, _)) ->
- Some (id, Manual, (set_maximality imps' b, fi))
+ begin match autoimp, explimp.CAst.v with
+ | (Name id,_), Some (_,max) ->
+ Some (id, Manual, (set_maximality imps' max, true))
| (Name id,Some exp), None when enriching ->
Some (id, exp, (set_maximality imps' flags.maximal, true))
| (Name _,_), None -> None
- | (Anonymous,_), Some (Some id, (b, fi, true)) ->
- Some (id,Manual,(b,fi))
- | (Anonymous,_), Some (None, (b, fi, true)) ->
+ | (Anonymous,_), Some (Name id,max) ->
+ Some (id,Manual,(max,true))
+ | (Anonymous,_), Some (Anonymous,max) ->
let id = Id.of_string ("arg_" ^ string_of_int k) in
- Some (id,Manual,(b,fi))
- | (Anonymous,_), Some (_, (_, _, false)) -> None
+ Some (id,Manual,(max,true))
| (Anonymous,_), None -> None
end :: imps'
| [], [] -> []
- (* flatten_explicitations returns a list of the same length as autoimps *)
- | _ -> assert false
- in merge 1 autoimps (flatten_explicitations l autoimps)
+ | [], _ -> assert false
+ (* possibly more automatic than manual implicit arguments n
+ when the conclusion is an unfoldable constant *)
+ | autoimps, [] -> merge k autoimps [CAst.make None]
+ in merge 1 autoimps l
let compute_semi_auto_implicits env sigma f t =
if not f.auto then [DefaultImpArgs, []]
@@ -642,9 +594,7 @@ let declare_mib_implicits kn =
(inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
(* Declare manual implicits *)
-type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
-
-type manual_implicits = manual_explicitation list
+type manual_implicits = (Name.t * bool) option CAst.t list
let compute_implicits_with_manual env sigma typ enriching l =
let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
@@ -669,8 +619,6 @@ let projection_implicits env p impls =
CList.skipn_at_least npars impls
let declare_manual_implicits local ref ?enriching l =
- assert (List.for_all (fun (_, (max, fi, fu)) -> fi && fu) l);
- assert (List.for_all (fun (ex, _) -> match ex with ExplByPos (_,_) -> true | _ -> false) l);
let flags = !implicit_args in
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -685,9 +633,8 @@ let declare_manual_implicits local ref ?enriching l =
in add_anonymous_leaf (inImplicits (req,[ref,l]))
let maybe_declare_manual_implicits local ref ?enriching l =
- match l with
- | [] -> ()
- | _ -> declare_manual_implicits local ref ?enriching l
+ if List.exists (fun x -> x.CAst.v <> None) l then
+ declare_manual_implicits local ref ?enriching l
(* TODO: either turn these warnings on and document them, or handle these cases sensibly *)
@@ -750,12 +697,6 @@ let extract_impargs_data impls =
| [] -> [] in
aux 0 impls
-let lift_implicits n =
- List.map (fun x ->
- match fst x with
- ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
- | _ -> x)
-
let make_implicits_list l = [DefaultImpArgs, l]
let rec drop_first_implicits p l =
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 1099074c63..92b6bdd406 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -84,13 +84,7 @@ val force_inference_of : implicit_status -> bool
val positions_of_implicits : implicits_list -> int list
-(** A [manual_explicitation] is a tuple of a positional or named explicitation with
- maximal insertion, force inference and force usage flags. Forcing usage makes
- the argument implicit even if the automatic inference considers it not inferable. *)
-type manual_explicitation = Constrexpr.explicitation *
- (maximal_insertion * force_inference * bool)
-
-type manual_implicits = manual_explicitation list
+type manual_implicits = (Name.t * bool) option CAst.t list
val compute_implicits_with_manual : env -> Evd.evar_map -> types -> bool ->
manual_implicits -> implicit_status list
@@ -131,8 +125,6 @@ val implicits_of_global : GlobRef.t -> implicits_list list
val extract_impargs_data :
implicits_list list -> ((int * int) option * implicit_status list) list
-val lift_implicits : int -> manual_implicits -> manual_implicits
-
val make_implicits_list : implicit_status list -> implicits_list list
val drop_first_implicits : int -> implicits_list -> implicits_list
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index bac46c2d2f..bab9024415 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -257,32 +257,23 @@ let warn_ignoring_implicit_status =
Name.print na ++ strbrk " and following binders")
let implicits_of_glob_constr ?(with_products=true) l =
- let add_impl i na bk l = match bk with
- | Implicit ->
- let name =
- match na with
- | Name id -> Some id
- | Anonymous -> None
- in
- (ExplByPos (i, name), (true, true, true)) :: l
- | _ -> l
+ let add_impl ?loc na bk l = match bk with
+ | Implicit -> CAst.make ?loc (Some (na,true)) :: l
+ | _ -> CAst.make ?loc None :: l
in
- let rec aux i c =
- let abs na bk b =
- add_impl i na bk (aux (succ i) b)
- in
+ let rec aux c =
match DAst.get c with
| GProd (na, bk, t, b) ->
- if with_products then abs na bk b
+ if with_products then add_impl na bk (aux b)
else
let () = match bk with
| Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
| _ -> ()
in []
- | GLambda (na, bk, t, b) -> abs na bk b
- | GLetIn (na, b, t, c) -> aux i c
+ | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b)
+ | GLetIn (na, b, t, c) -> aux c
| GRec (fix_kind, nas, args, tys, bds) ->
let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
- List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
+ List.fold_right (fun (na,bk,t,_) l -> add_impl ?loc:c.CAst.loc na bk l) args.(nb) (aux bds.(nb))
| _ -> []
- in aux 1 l
+ in aux l
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b64af52b6e..bd5a211f1d 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -537,8 +537,7 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
in
let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
let sigma, (c', imps') = interp_type_evars_impls ~program_mode ~impls env' sigma tclass in
- let len = Context.Rel.nhyps ctx in
- let imps = imps @ Impargs.lift_implicits len imps' in
+ let imps = imps @ imps' in
let ctx', c = decompose_prod_assum sigma c' in
let ctx'' = ctx' @ ctx in
let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 591e4b130f..a27c08d176 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -283,8 +283,8 @@ let context poly l =
Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
status
else
- let test (x, _) = match x with
- | Constrexpr.ExplByPos (_, Some id') -> Id.equal id id'
+ let test x = match x.CAst.v with
+ | Some (Name id',_) -> Id.equal id id'
| _ -> false
in
let impl = List.exists test impls in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 1046e354a7..ae1f55acda 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -27,18 +27,19 @@ let warn_implicits_in_term =
CWarnings.create ~name:"implicits-in-term" ~category:"implicits"
(fun () ->
strbrk "Implicit arguments declaration relies on type." ++ spc () ++
- strbrk "The term declares more implicits than the type here.")
+ strbrk "Discarding incompatible declaration in term.")
let check_imps ~impsty ~impsbody =
- let b =
- try
- List.for_all (fun (key, (va:bool*bool*bool)) ->
- (* Pervasives.(=) is OK for this type *)
- Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va)
- impsbody
- with Not_found -> false
- in
- if not b then warn_implicits_in_term ()
+ let rec aux impsty impsbody =
+ match impsty, impsbody with
+ | a1 :: impsty, a2 :: impsbody ->
+ (match a1.CAst.v, a2.CAst.v with
+ | None , None -> aux impsty impsbody
+ | Some _ , Some _ -> aux impsty impsbody
+ | _, _ -> warn_implicits_in_term ?loc:a2.CAst.loc ())
+ | _ :: _, [] | [], _ :: _ -> (* Information only on one side *) ()
+ | [], [] -> () in
+ aux impsty impsbody
let interp_definition ~program_mode pl bl poly red_option c ctypopt =
let env = Global.env() in
@@ -56,11 +57,11 @@ let interp_definition ~program_mode pl bl poly red_option c ctypopt =
match tyopt with
| None ->
let evd, (c, impsbody) = interp_constr_evars_impls ~program_mode ~impls env_bl evd c in
- evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None
+ evd, c, imps1@impsbody, None
| Some (ty, impsty) ->
let evd, (c, impsbody) = interp_casted_constr_evars_impls ~program_mode ~impls env_bl evd c ty in
check_imps ~impsty ~impsbody;
- evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
+ evd, c, imps1@impsty, Some ty
in
(* Do the reduction *)
let evd, c = red_constant_body red_option env_bl evd c in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 6068cd90f1..0d7ba69955 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -197,7 +197,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in
let fiximps = List.map3
- (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps))
+ (fun ctximps cclimps (_,ctx) -> ctximps@cclimps)
fixctximps fixcclimps fixctxs in
let sigma, rec_sign =
List.fold_left2
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a31f3c34e0..1ded9f3d29 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -57,7 +57,7 @@ val interp_recursive :
(* names / defs / types *)
(Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) *
(* ctx per mutual def / implicits / struct annotations *)
- (EConstr.rel_context * Impargs.manual_explicitation list * int option) list
+ (EConstr.rel_context * Impargs.manual_implicits * int option) list
(** Exported for Funind *)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5bebf955ec..2f8b12f4c5 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -375,8 +375,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
(* Compute interpretation metadatas *)
- let indimpls = List.map (fun impls -> userimpls @
- lift_implicits (Context.Rel.nhyps ctx_params) impls) indimpls in
+ let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in
let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
@@ -402,8 +401,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
constructors
in
let ctx_params = ctx_params @ ctx_uparams in
- let userimpls = useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) userimpls) in
- let indimpls = List.map (fun iimpl -> useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) iimpl)) indimpls in
+ let userimpls = useruimpls @ userimpls in
+ let indimpls = List.map (fun iimpl -> useruimpls @ iimpl) indimpls in
let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in
let env_ar = push_types env0 indnames relevances fullarities in
let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
@@ -450,10 +449,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
indl arities arityconcl constructors
in
let impls =
- let len = Context.Rel.nhyps ctx_params in
List.map2 (fun indimpls (_,_,cimpls) ->
indimpls, List.map (fun impls ->
- userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
+ userimpls @ impls) cimpls) indimpls constructors
in
let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in
(* Build the mutual inductive entry *)
@@ -559,8 +557,8 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p
mind
type one_inductive_impls =
- Impargs.manual_explicitation list (* for inds *)*
- Impargs.manual_explicitation list list (* for constrs *)
+ Impargs.manual_implicits (* for inds *) *
+ Impargs.manual_implicits list (* for constrs *)
type uniform_inductive_flag =
| UniformParameters
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index a7366b2c56..7aba64fb93 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -469,7 +469,7 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
(* XXX: The nf_evar is critical !! *)
evd, (id.CAst.v,
(Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
- (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
+ (ids, imps @ imps'))))
evd thms in
let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in
let evd = Evd.minimize_universes evd in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index ac647af8b5..25c5b24e91 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -112,7 +112,7 @@ val start_lemma_with_initialization
-> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option
-> (Id.t (* name of thm *) *
(EConstr.types (* type of thm *) *
- (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
+ (Name.t list (* names to pre-introduce *) * Impargs.manual_implicits))) list
-> int list option
-> t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 50d24c20c9..6ef2f80067 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -307,7 +307,7 @@ type program_info_aux = {
prg_obligations: obligations;
prg_deps : Id.t list;
prg_fixkind : fixpoint_kind option ;
- prg_implicits : (Constrexpr.explicitation * (bool * bool * bool)) list;
+ prg_implicits : Impargs.manual_implicits;
prg_notations : notations ;
prg_kind : definition_kind;
prg_reduce : constr -> constr;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 8734d82970..18a7e10733 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -57,7 +57,7 @@ val add_definition
-> ?term:constr -> types
-> UState.t
-> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
- -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list
+ -> ?implicits:Impargs.manual_implicits
-> ?kind:Decl_kinds.definition_kind
-> ?tactic:unit Proofview.tactic
-> ?reduce:(constr -> constr)
@@ -74,8 +74,7 @@ type fixpoint_kind =
| IsCoFixpoint
val add_mutual_definitions :
- (Names.Id.t * constr * types *
- (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
+ (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list ->
UState.t ->
?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
?tactic:unit Proofview.tactic ->
diff --git a/vernac/record.ml b/vernac/record.ml
index c777ef2c2b..48cde133a8 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -476,21 +476,15 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
List.mapi map record_data
let implicits_of_context ctx =
- List.map_i (fun i name ->
- let explname =
- match name with
- | Name n -> Some n
- | Anonymous -> None
- in ExplByPos (i, explname), (true, true, true))
- 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
+ List.map (fun name -> CAst.make (Some (name,true)))
+ (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
let declare_class def cum ubinders univs id idbuild paramimpls params arity
template fieldimpls fields ?(kind=StructureComponent) coers priorities =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
- 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
+ List.map (fun x -> impls @ x) fieldimpls
in
let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in
let data =
@@ -704,7 +698,7 @@ let definition_structure udecl kind ~template cum poly finite records =
declare_class def cum ubinders univs id.CAst.v idbuild
implpars params arity template implfs fields coers priorities
| _ ->
- let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
+ let map impls = implpars @ [CAst.make None] @ impls in
let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:26:36 +0000