aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh6
-rw-r--r--dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh9
-rw-r--r--doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst9
-rw-r--r--doc/sphinx/addendum/extraction.rst5
-rw-r--r--interp/impargs.ml30
-rw-r--r--tactics/auto.ml3
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/hints.ml120
-rw-r--r--tactics/hints.mli2
-rw-r--r--test-suite/bugs/closed/bug_12001.v24
-rw-r--r--test-suite/output/Arguments_renaming.out2
-rw-r--r--test-suite/output/Arguments_renaming.v1
-rw-r--r--test-suite/output/Implicit.out2
-rw-r--r--test-suite/output/RecordMissingField.out20
-rw-r--r--test-suite/output/RecordMissingField.v8
-rw-r--r--test-suite/success/Typeclasses.v2
-rw-r--r--vernac/comArguments.ml8
-rw-r--r--vernac/declare.ml22
-rw-r--r--vernac/declare.mli3
20 files changed, 186 insertions, 94 deletions
diff --git a/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh b/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh
new file mode 100644
index 0000000000..56a69abbf7
--- /dev/null
+++ b/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12709" ] || [ "$CI_BRANCH" = "hint-pattern-out" ]; then
+
+ coqhammer_CI_REF=hint-pattern-out
+ coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
+
+fi
diff --git a/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh
new file mode 100644
index 0000000000..54fdd87566
--- /dev/null
+++ b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "12756" ] || [ "$CI_BRANCH" = "dont-refresh-argument-names" ]; then
+
+ mathcomp_CI_REF=dont-refresh-argument-names-overlay
+ mathcomp_CI_GITURL=https://github.com/jashug/math-comp
+
+ oddorder_CI_REF=dont-refresh-argument-names-overlay
+ oddorder_CI_GITURL=https://github.com/jashug/odd-order
+
+fi
diff --git a/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst b/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst
new file mode 100644
index 0000000000..b0cf4ca4e3
--- /dev/null
+++ b/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst
@@ -0,0 +1,9 @@
+- **Changed:**
+ Tweaked the algorithm giving default names to arguments.
+ Should reduce the frequency that argument names get an
+ unexpected suffix.
+ Also makes :flag:`Mangle Names` not mess up argument names.
+ (`#12756 <https://github.com/coq/coq/pull/12756>`_,
+ fixes `#12001 <https://github.com/coq/coq/issues/12001>`_
+ and `#6785 <https://github.com/coq/coq/issues/6785>`_,
+ by Jasper Hugunin).
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 41b726b069..ce68274036 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -99,12 +99,15 @@ Extraction Options
Setting the target language
~~~~~~~~~~~~~~~~~~~~~~~~~~~
-.. cmd:: Extraction Language {| OCaml | Haskell | Scheme }
+.. cmd:: Extraction Language {| OCaml | Haskell | Scheme | JSON }
:name: Extraction Language
The ability to fix target language is the first and more important
of the extraction options. Default is ``OCaml``.
+ The JSON output is mostly for development or debugging:
+ it contains the raw ML term produced as an intermediary target.
+
Inlining and optimizations
~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/interp/impargs.ml b/interp/impargs.ml
index db102470b0..48961c6c8a 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,7 +20,6 @@ open Lib
open Libobject
open EConstr
open Reductionops
-open Namegen
open Constrexpr
module NamedDecl = Context.Named.Declaration
@@ -247,24 +246,15 @@ let is_rigid env sigma t =
is_rigid_head sigma t
| _ -> true
-let find_displayed_name_in sigma all avoid na (env, b) =
- let envnames_b = (env, b) in
- let flag = RenamingElsewhereFor envnames_b in
- if all then compute_and_force_displayed_name_in sigma flag avoid na b
- else compute_displayed_name_in sigma flag avoid na b
-
-let compute_implicits_names_gen all env sigma t =
+let compute_implicits_names env sigma t =
let open Context.Rel.Declaration in
- let rec aux env avoid names t =
+ let rec aux env names t =
let t = whd_all env sigma t in
match kind sigma t with
| Prod (na,a,b) ->
- let na',avoid' = find_displayed_name_in sigma all avoid na.Context.binder_name (names,b) in
- aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b
+ aux (push_rel (LocalAssum (na,a)) env) (na.Context.binder_name::names) b
| _ -> List.rev names
- in aux env Id.Set.empty [] t
-
-let compute_implicits_names = compute_implicits_names_gen true
+ in aux env [] t
let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t =
let open Context.Rel.Declaration in
@@ -291,9 +281,9 @@ let compute_implicits_explanation_flags env sigma f t =
(f.strict || f.strongly_strict) f.strongly_strict
f.reversible_pattern f.contextual env sigma t
-let compute_implicits_flags env sigma f all t =
+let compute_implicits_flags env sigma f t =
List.combine
- (compute_implicits_names_gen all env sigma t)
+ (compute_implicits_names env sigma t)
(compute_implicits_explanation_flags env sigma f t)
let compute_auto_implicits env sigma flags enriching t =
@@ -361,10 +351,10 @@ let positions_of_implicits (_,impls) =
let rec prepare_implicits i f = function
| [] -> []
- | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
- | (Name id, Some imp)::imps ->
+ | (na, Some imp)::imps ->
let imps' = prepare_implicits (i+1) f imps in
- Some (ExplByName id,imp,(set_maximality Silent (Name id) i imps' f.maximal,true)) :: imps'
+ let expl = match na with Name id -> ExplByName id | Anonymous -> ExplByPos (i,None) in
+ Some (expl,imp,(set_maximality Silent na i imps' f.maximal,true)) :: imps'
| _::imps -> None :: prepare_implicits (i+1) f imps
let set_manual_implicits silent flags enriching autoimps l =
@@ -393,7 +383,7 @@ let set_manual_implicits silent flags enriching autoimps l =
let compute_semi_auto_implicits env sigma f t =
if not f.auto then [DefaultImpArgs, []]
- else let l = compute_implicits_flags env sigma f false t in
+ else let l = compute_implicits_flags env sigma f t in
[DefaultImpArgs, prepare_implicits 1 f l]
(*s Constants. *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0931c3e61e..488bcb5208 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -369,8 +369,7 @@ and tac_of_hint dbg db_list local_db concl (flags, h) =
let info = Exninfo.reify () in
Tacticals.New.tclFAIL ~info 0 (str"Unbound reference")
end
- | Extern tacast ->
- let p = FullHint.pattern h in
+ | Extern (p, tacast) ->
conclPattern concl p tacast
in
let pr_hint env sigma =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 36544883aa..378a3e718b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -359,7 +359,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
Tacticals.New.tclTHEN fst snd
| Unfold_nth c ->
Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
- | Extern tacast -> conclPattern concl p tacast
+ | Extern (p, tacast) -> conclPattern concl p tacast
in
let tac = FullHint.run h tac in
let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 9a554b117e..17e6a6edb4 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -126,7 +126,7 @@ and e_my_find_search env sigma db_list local_db secvars concl =
Tacticals.New.tclTHEN (unify_e_resolve st h)
(e_trivial_fail_db db_list local_db)
| Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
- | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast
+ | Extern (pat, tacast) -> conclPattern concl pat tacast
in
let tac = FullHint.run h tac in
(tac, b, lazy (FullHint.print env sigma h))
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 41b200bb83..4532f97a27 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -42,21 +42,22 @@ type debug = Debug | Info | Off
exception Bound
-let head_constr_bound sigma t =
- let t = strip_outer_cast sigma t in
- let _,ccl = decompose_prod_assum sigma t in
- let hd,args = decompose_app sigma ccl in
- let open GlobRef in
- match EConstr.kind sigma hd with
- | Const (c, _) -> ConstRef c
- | Ind (i, _) -> IndRef i
- | Construct (c, _) -> ConstructRef c
- | Var id -> VarRef id
- | Proj (p, _) -> ConstRef (Projection.constant p)
- | _ -> raise Bound
+let rec head_bound sigma t = match EConstr.kind sigma t with
+| Prod (_, _, b) -> head_bound sigma b
+| LetIn (_, _, _, b) -> head_bound sigma b
+| App (c, _) -> head_bound sigma c
+| Case (_, _, _, c, _) -> head_bound sigma c
+| Ind (ind, _) -> GlobRef.IndRef ind
+| Const (c, _) -> GlobRef.ConstRef c
+| Construct (c, _) -> GlobRef.ConstructRef c
+| Var id -> GlobRef.VarRef id
+| Proj (p, _) -> GlobRef.ConstRef (Projection.constant p)
+| Cast (c, _, _) -> head_bound sigma c
+| Evar _ | Rel _ | Meta _ | Sort _ | Fix _ | Lambda _
+| CoFix _ | Int _ | Float _ | Array _ -> raise Bound
let head_constr sigma c =
- try head_constr_bound sigma c
+ try head_bound sigma c
with Bound -> user_err (Pp.str "Head identifier must be a constant, section variable, \
(co)inductive type, (co)inductive type constructor, or projection.")
@@ -105,7 +106,7 @@ type 'a hint_ast =
| Give_exact of 'a
| Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
| Unfold_nth of evaluable_global_reference (* Hint Unfold *)
- | Extern of Genarg.glob_generic_argument (* Hint Extern *)
+ | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument (* Hint Extern *)
type 'a hints_path_atom_gen =
@@ -237,10 +238,38 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0
type stored_data = int * full_hint
(* First component is the index of insertion in the table, to keep most recent first semantics. *)
-module Bounded_net = Btermdn.Make(struct
- type t = stored_data
- let compare = pri_order_int
- end)
+module Bounded_net :
+sig
+ type t
+ val empty : t
+ val add : TransparentState.t option -> t -> Pattern.constr_pattern -> stored_data -> t
+ val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> stored_data list
+end =
+struct
+ module Data = struct type t = stored_data let compare = pri_order_int end
+ module Bnet = Btermdn.Make(Data)
+
+ type diff = TransparentState.t option * Pattern.constr_pattern * stored_data
+ type data = Bnet of Bnet.t | Diff of diff * data ref
+ type t = data ref
+
+ let empty = ref (Bnet Bnet.empty)
+
+ let add st net p v = ref (Diff ((st, p, v), net))
+
+ let rec force net = match !net with
+ | Bnet dn -> dn
+ | Diff ((st, p, v), rem) ->
+ let dn = force rem in
+ let p = Bnet.pattern st p in
+ let dn = Bnet.add dn p v in
+ let () = net := (Bnet dn) in
+ dn
+
+ let lookup sigma st net p =
+ let dn = force net in
+ Bnet.lookup sigma st dn p
+end
type search_entry = {
sentry_nopat : stored_data list;
@@ -263,18 +292,17 @@ let add_tac pat t se =
| None ->
if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se
else { se with sentry_nopat = List.insert pri_order t se.sentry_nopat }
- | Some pat ->
+ | Some (st, pat) ->
if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se
else { se with
sentry_pat = List.insert pri_order t se.sentry_pat;
- sentry_bnet = Bounded_net.add se.sentry_bnet pat t; }
+ sentry_bnet = Bounded_net.add st se.sentry_bnet pat t; }
let rebuild_dn st se =
let dn' =
List.fold_left
(fun dn (id, t) ->
- let pat = Bounded_net.pattern (Some st) (Option.get t.pat) in
- Bounded_net.add dn pat (id, t))
+ Bounded_net.add (Some st) dn (Option.get t.pat) (id, t))
Bounded_net.empty se.sentry_pat
in
{ se with sentry_bnet = dn' }
@@ -322,8 +350,7 @@ let instantiate_hint env sigma p =
| Res_pf_THEN_trivial_fail c ->
Res_pf_THEN_trivial_fail (mk_clenv c)
| Give_exact c -> Give_exact (mk_clenv c)
- | Unfold_nth e -> Unfold_nth e
- | Extern t -> Extern t
+ | (Unfold_nth _ | Extern _) as h -> h
in
{ p with code = { p.code with obj = code } }
@@ -650,7 +677,7 @@ struct
if not db.use_dn && is_exact v.code.obj then None
else
let dnst = if db.use_dn then Some db.hintdb_state else None in
- Option.map (fun p -> Bounded_net.pattern dnst p) v.pat
+ Option.map (fun p -> (dnst, p)) v.pat
in
let oval = find gr db in
{ db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv oval) db.hintdb_map }
@@ -775,12 +802,6 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with
(* adding and removing tactics in the search table *)
-let try_head_pattern c =
- try head_pattern_bound c
- with BoundPattern ->
- user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \
- an if, case, or let expression, an application, or a projection.")
-
let with_uid c = { obj = c; uid = fresh_key () }
let secvars_of_idset s =
@@ -801,15 +822,15 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
match EConstr.kind sigma cty with
| Prod _ -> failwith "make_exact_entry"
| _ ->
- let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in
let hd =
- try head_pattern_bound pat
- with BoundPattern -> failwith "make_exact_entry"
+ try head_bound sigma cty
+ with Bound -> failwith "make_exact_entry"
in
let pri = match info.hint_priority with None -> 0 | Some p -> p in
let pat = match info.hint_pattern with
| Some pat -> snd pat
- | None -> pat
+ | None ->
+ Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty)
in
(Some hd,
{ pri; pat = Some pat; name;
@@ -823,16 +844,17 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (
let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
let ce = mk_clenv_from_env env sigma' None (c,cty) in
let c' = clenv_type (* ~reduce:false *) ce in
- let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in
let hd =
- try head_pattern_bound pat
- with BoundPattern -> failwith "make_apply_entry" in
+ try head_bound ce.evd c'
+ with Bound -> failwith "make_apply_entry" in
let miss = clenv_missing ce in
let nmiss = List.length miss in
let secvars = secvars_of_constr env sigma c in
let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in
let pat = match info.hint_pattern with
- | Some p -> snd p | None -> pat
+ | Some p -> snd p
+ | None ->
+ Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c')
in
if Int.equal nmiss 0 then
(Some hd,
@@ -935,14 +957,21 @@ let make_unfold eref =
code = with_uid (Unfold_nth eref) })
let make_extern pri pat tacast =
- let hdconstr = Option.map try_head_pattern pat in
+ let hdconstr = match pat with
+ | None -> None
+ | Some c ->
+ try Some (head_pattern_bound c)
+ with BoundPattern ->
+ user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \
+ an if, case, or let expression, an application, or a projection.")
+ in
(hdconstr,
{ pri = pri;
pat = pat;
name = PathAny;
db = None;
secvars = Id.Pred.empty; (* Approximation *)
- code = with_uid (Extern tacast) })
+ code = with_uid (Extern (pat, tacast)) })
let make_mode ref m =
let open Term in
@@ -1076,7 +1105,7 @@ let subst_autohint (subst, obj) =
match t with
| None -> gr'
| Some t ->
- (try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
+ (try head_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
with Bound -> gr')
in
let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
@@ -1106,9 +1135,10 @@ let subst_autohint (subst, obj) =
| Unfold_nth ref ->
let ref' = subst_evaluable_reference subst ref in
if ref==ref' then data.code.obj else Unfold_nth ref'
- | Extern tac ->
+ | Extern (pat, tac) ->
+ let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in
let tac' = Genintern.generic_substitute subst tac in
- if tac==tac' then data.code.obj else Extern tac'
+ if pat==pat' && tac==tac' then data.code.obj else Extern (pat', tac')
in
let name' = subst_path_atom subst data.name in
let uid' = subst_kn subst data.code.uid in
@@ -1388,7 +1418,7 @@ let pr_hint env sigma h = match h.obj with
(str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial")
| Unfold_nth c ->
str"unfold " ++ pr_evaluable_reference c
- | Extern tac ->
+ | Extern (_, tac) ->
str "(*external*) " ++ Pputils.pr_glb_generic env sigma tac
let pr_id_hint env sigma (id, v) =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index f0fed75828..0b9da27ab3 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -37,7 +37,7 @@ type 'a hint_ast =
| Give_exact of 'a
| Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
| Unfold_nth of evaluable_global_reference (* Hint Unfold *)
- | Extern of Genarg.glob_generic_argument (* Hint Extern *)
+ | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument (* Hint Extern *)
type hint = private {
hint_term : constr;
diff --git a/test-suite/bugs/closed/bug_12001.v b/test-suite/bugs/closed/bug_12001.v
new file mode 100644
index 0000000000..19533e49f1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12001.v
@@ -0,0 +1,24 @@
+(* Argument names don't get mangled *)
+Set Mangle Names.
+Lemma leibniz_equiv_iff {A : Type} (x y : A) : True.
+Proof. tauto. Qed.
+Check leibniz_equiv_iff (A := nat) 2 3 : True.
+Unset Mangle Names.
+
+(* Coq doesn't make up names for arguments *)
+Definition bar (a a : nat) : nat := 3.
+Arguments bar _ _ : assert.
+Fail Arguments bar a a0 : assert.
+
+(* This definition caused an anomaly in a version of this PR
+without the change to prepare_implicits *)
+Set Implicit Arguments.
+Definition foo (_ : nat) (_ : @eq nat ltac:(assumption) 2) : True := I.
+Fail Check foo (H := 2).
+
+Definition baz (a b : nat) := b.
+Arguments baz a {b}.
+Set Mangle Names.
+Definition baz2 (a b : nat) := b.
+Arguments baz2 a {b}.
+Unset Mangle Names.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index e0aa758812..c28bb14eb3 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -84,8 +84,6 @@ Argument lists should agree on the names they provide.
The command has indeed failed with message:
Sequences of implicit arguments must be of different lengths.
The command has indeed failed with message:
-Some argument names are duplicated: F
-The command has indeed failed with message:
Argument number 3 is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].
The command has indeed failed with message:
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index 6ac09cf771..6001850046 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -48,7 +48,6 @@ Check @myplus.
Fail Arguments eq_refl {F g}, [H] k.
Fail Arguments eq_refl {F}, [F] : rename.
-Fail Arguments eq_refl {F F}, [F] F : rename.
Fail Arguments eq {A} x [z] : rename.
Fail Arguments eq {F} x z y.
Fail Arguments eq {R} s t.
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index ef7667936c..2265028d3e 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
d2 = fun x : nat => d1 (y:=x)
: forall x x0 : nat, x0 = x -> x0 = x
-Arguments d2 [x x0]%nat_scope
+Arguments d2 [x x]%nat_scope
map id (1 :: nil)
: list nat
map id' (1 :: nil)
diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out
index 7c80a6065f..28beee90b2 100644
--- a/test-suite/output/RecordMissingField.out
+++ b/test-suite/output/RecordMissingField.out
@@ -1,4 +1,16 @@
-File "stdin", line 8, characters 5-22:
-Error: Cannot infer field y2p of record point2d in environment:
-p : point2d
-
+The command has indeed failed with message:
+The following term contains unresolved implicit arguments:
+ (fun p : point2d => {| x2p := x2p p + 1; y2p := ?y2p |})
+More precisely:
+- ?y2p: Cannot infer field y2p of record point2d in environment:
+ p : point2d
+The command has indeed failed with message:
+The following term contains unresolved implicit arguments:
+ (fun p : point2d => {| x2p := x2p p + (fun n : nat => ?n) 1; y2p := ?y2p |})
+More precisely:
+- ?n: Cannot infer this placeholder of type "nat" in
+ environment:
+ p : point2d
+ n : nat
+- ?y2p: Cannot infer field y2p of record point2d in environment:
+ p : point2d
diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v
index 84f1748fa0..8ca721564b 100644
--- a/test-suite/output/RecordMissingField.v
+++ b/test-suite/output/RecordMissingField.v
@@ -3,6 +3,10 @@ should contain missing field, and the inferred type of the record **)
Record point2d := mkPoint { x2p: nat; y2p: nat }.
-
-Definition increment_x (p: point2d) : point2d :=
+Fail Definition increment_x (p: point2d) : point2d :=
{| x2p := x2p p + 1; |}.
+
+(* Here there is also an unresolved implicit, which should give an
+ understadable error as well *)
+Fail Definition increment_x (p: point2d) : point2d :=
+ {| x2p := x2p p + (fun n => _) 1; |}.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 563651cfa5..7acaa92b89 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -190,7 +190,7 @@ Record Monad {m : Type -> Type} := {
Print Visibility.
Print unit.
-Arguments unit {m m0 α}.
+Arguments unit {m _ α}.
Arguments Monad : clear implicits.
Notation "'return' t" := (unit t).
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index 360e228bfc..be9cc059a7 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -213,14 +213,6 @@ let vernac_arguments ~section_local reference args more_implicits flags =
in CErrors.user_err ~hdr:"vernac_declare_arguments" msg
end;
- let duplicate_names =
- List.duplicates Name.equal (List.filter ((!=) Anonymous) names)
- in
- if not (List.is_empty duplicate_names) then begin
- CErrors.user_err Pp.(strbrk "Some argument names are duplicated: " ++
- prlist_with_sep pr_comma Name.print duplicate_names)
- end;
-
let implicits =
List.map (fun { name; implicit_status = i } -> (name,i)) args
in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index eedbee852b..66537c2978 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -642,14 +642,32 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
dref
(* Preparing proof entries *)
+let error_unresolved_evars env sigma t evars =
+ let pr_unresolved_evar e =
+ hov 2 (str"- " ++ Printer.pr_existential_key sigma e ++ str ": " ++
+ Himsg.explain_pretype_error env sigma
+ (Pretype_errors.UnsolvableImplicit (e,None)))
+ in
+ CErrors.user_err (hov 0 begin
+ str "The following term contains unresolved implicit arguments:"++ fnl () ++
+ str " " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++
+ str "More precisely: " ++ fnl () ++
+ v 0 (prlist_with_sep cut pr_unresolved_evar (Evar.Set.elements evars))
+ end)
+
+let check_evars_are_solved env sigma t =
+ let t = EConstr.of_constr t in
+ let evars = Evarutil.undefined_evars_of_term sigma t in
+ if not (Evar.Set.is_empty evars) then error_unresolved_evars env sigma t evars
let prepare_definition ~info ~opaque ~body ~typ sigma =
let { Info.poly; udecl; inline; _ } = info in
let env = Global.env () in
- Pretyping.check_evars_are_solved ~program_mode:false env sigma;
- let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
+ let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
sigma (fun nf -> nf body, Option.map nf typ)
in
+ Option.iter (check_evars_are_solved env sigma) types;
+ check_evars_are_solved env sigma body;
let univs = Evd.check_univ_decl ~poly sigma udecl in
let entry = definition_entry ~opaque ~inline ?types ~univs body in
let uctx = Evd.evar_universe_context sigma in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index c5a8afbad5..3001d0d206 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -117,8 +117,7 @@ end
normalized w.r.t. the passed [evar_map] [sigma]. Universes should
be handled properly, including minimization and restriction. Note
that [sigma] is checked for unresolved evars, thus you should be
- careful not to submit open terms or evar maps with stale,
- unresolved existentials *)
+ careful not to submit open terms *)
val declare_definition
: info:Info.t
-> cinfo:EConstr.t option CInfo.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 23:02:23 +0000