aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml2
-rw-r--r--interp/constrintern.mli4
-rw-r--r--interp/impargs.ml11
-rw-r--r--interp/impargs.mli2
-rw-r--r--interp/implicit_quantifiers.ml12
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comDefinition.ml19
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/comInductive.ml4
-rw-r--r--vernac/lemmas.mli2
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/obligations.mli5
-rw-r--r--vernac/record.ml2
13 files changed, 35 insertions, 34 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1a81dc41a1..622a9aee3d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2437,7 +2437,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
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
+ CAst.make (ExplByPos (n, na), (true, true, true)) :: impls
else impls
in
(push_rel d env, sigma, d::params, succ n, impls)
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..81fe3e22b3 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -369,6 +369,7 @@ let check_correct_manual_implicits autoimps l =
(* Take a list l of explicitations, and map them to positions. *)
let flatten_explicitations l autoimps =
+ let l = List.map (fun c -> c.CAst.v) l in
let rec aux k l = function
| (Name id,_)::imps ->
let value, l' =
@@ -644,7 +645,7 @@ let declare_mib_implicits kn =
(* Declare manual implicits *)
type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
-type manual_implicits = manual_explicitation list
+type manual_implicits = manual_explicitation 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 +670,8 @@ 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);
+ assert (List.for_all (fun {CAst.v=(_, (max, fi, fu))} -> fi && fu) l);
+ assert (List.for_all (fun {CAst.v=(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
@@ -751,10 +752,10 @@ let extract_impargs_data impls =
aux 0 impls
let lift_implicits n =
- List.map (fun x ->
+ List.map (CAst.map (fun x ->
match fst x with
ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
- | _ -> x)
+ | _ -> x))
let make_implicits_list l = [DefaultImpArgs, l]
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 1099074c63..07f015d319 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -90,7 +90,7 @@ val positions_of_implicits : implicits_list -> int list
type manual_explicitation = Constrexpr.explicitation *
(maximal_insertion * force_inference * bool)
-type manual_implicits = manual_explicitation list
+type manual_implicits = manual_explicitation CAst.t list
val compute_implicits_with_manual : env -> Evd.evar_map -> types -> bool ->
manual_implicits -> implicit_status list
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index bac46c2d2f..34674fb102 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -257,19 +257,19 @@ 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
+ let add_impl ?loc 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
+ CAst.make ?loc (ExplByPos (i, name), (true, true, true)) :: l
| _ -> l
in
let rec aux i c =
- let abs na bk b =
- add_impl i na bk (aux (succ i) b)
+ let abs ?loc na bk b =
+ add_impl ?loc i na bk (aux (succ i) b)
in
match DAst.get c with
| GProd (na, bk, t, b) ->
@@ -279,10 +279,10 @@ let implicits_of_glob_constr ?(with_products=true) l =
| Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
| _ -> ()
in []
- | GLambda (na, bk, t, b) -> abs na bk b
+ | GLambda (na, bk, t, b) -> abs ?loc:t.CAst.loc na bk b
| GLetIn (na, b, t, c) -> aux i 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_left_i (fun i l (na,bk,t,_) -> add_impl ?loc:c.CAst.loc i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
| _ -> []
in aux 1 l
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 591e4b130f..c1f676b043 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -283,7 +283,7 @@ 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
+ let test {CAst.v = (x, _)} = match x with
| Constrexpr.ExplByPos (_, Some id') -> Id.equal id id'
| _ -> false
in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 1046e354a7..01274e2568 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)) ->
+ let impsty = List.map (fun x -> x.CAst.v) impsty in
+ List.iter (fun {CAst.v = (key, (va:bool*bool*bool)); CAst.loc} ->
+ let b =
+ try
(* 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 ()
+ Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va
+ with Not_found -> false
+ in
+ if not b then warn_implicits_in_term ?loc ())
+ impsbody
let interp_definition ~program_mode pl bl poly red_option c ctypopt =
let env = Global.env() in
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..e0f2f05fe3 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -559,8 +559,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.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..e555c6d154 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -481,7 +481,7 @@ let implicits_of_context ctx =
match name with
| Name n -> Some n
| Anonymous -> None
- in ExplByPos (i, explname), (true, true, true))
+ in CAst.make (ExplByPos (i, explname), (true, true, true)))
1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
let declare_class def cum ubinders univs id idbuild paramimpls params arity
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:52:04 +0000