aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/04-tactics/12256-unfold-dyn-check.rst4
-rw-r--r--doc/sphinx/proof-engine/tactics.rst14
-rw-r--r--interp/notation.ml8
-rw-r--r--interp/notation.mli3
-rw-r--r--interp/smartlocate.ml8
-rw-r--r--plugins/ltac/tacintern.ml69
-rw-r--r--test-suite/bugs/closed/bug_11727.v8
-rw-r--r--test-suite/bugs/closed/bug_4925.v6
-rw-r--r--test-suite/bugs/closed/bug_5159.v12
-rw-r--r--test-suite/bugs/closed/bug_5764.v7
-rw-r--r--test-suite/success/with_strategy.v8
-rw-r--r--vernac/prettyp.ml4
-rw-r--r--vernac/vernacentries.ml2
13 files changed, 88 insertions, 65 deletions
diff --git a/doc/changelog/04-tactics/12256-unfold-dyn-check.rst b/doc/changelog/04-tactics/12256-unfold-dyn-check.rst
new file mode 100644
index 0000000000..c2f7065f4c
--- /dev/null
+++ b/doc/changelog/04-tactics/12256-unfold-dyn-check.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+ The check that unfold arguments were indeed unfoldable has been moved to runtime
+ (`#12256 <https://github.com/coq/coq/pull/12256>`_,
+ by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 127e4c6dbe..ad799fbbcd 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3393,17 +3393,6 @@ the conversion in hypotheses :n:`{+ @ident}`.
never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to
ensure that unfolding does not fail.
- .. note::
-
- This tactic unfortunately does not yet play well with tactic
- internalization, resulting in interpretation-time errors when
- you try to use it directly with opaque identifiers, as seen in
- the first (failing) use of :tacn:`with_strategy` in the
- following example. This can be worked around by binding the
- identifier to an |Ltac| variable, and this issue should
- disappear in a future version of |Coq|; see `#12179
- <https://github.com/coq/coq/issues/12179>`_.
-
.. example::
.. coqtop:: all reset abort
@@ -3411,8 +3400,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
Opaque id.
Goal id 10 = 10.
Fail unfold id.
- Fail with_strategy transparent [id] unfold id.
- let id' := id in with_strategy transparent [id] unfold id'.
+ with_strategy transparent [id] unfold id.
.. warning::
diff --git a/interp/notation.ml b/interp/notation.ml
index 2703930705..fb3cefd624 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1809,10 +1809,10 @@ let browse_notation strict ntn map =
map [] in
List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l
-let global_reference_of_notation test (ntn,(sc,c,_)) =
+let global_reference_of_notation ~head test (ntn,(sc,c,_)) =
match c with
| NRef ref when test ref -> Some (ntn,sc,ref)
- | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l && test ref ->
+ | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref ->
Some (ntn,sc,ref)
| _ -> None
@@ -1824,14 +1824,14 @@ let error_notation_not_reference ?loc ntn =
(str "Unable to interpret " ++ quote (str ntn) ++
str " as a reference.")
-let interp_notation_as_global_reference ?loc test ntn sc =
+let interp_notation_as_global_reference ?loc ~head test ntn sc =
let scopes = match sc with
| Some sc ->
let scope = find_scope (find_delimiters_scope sc) in
String.Map.add sc scope String.Map.empty
| None -> !scope_map in
let ntns = browse_notation true ntn scopes in
- let refs = List.map (global_reference_of_notation test) ntns in
+ let refs = List.map (global_reference_of_notation ~head test) ntns in
match Option.List.flatten refs with
| [_,_,ref] -> ref
| [] -> error_notation_not_reference ?loc ntn
diff --git a/interp/notation.mli b/interp/notation.mli
index b427aa9bb3..96a76c4de6 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -245,7 +245,8 @@ val availability_of_notation : specific_notation -> subscopes ->
(** {6 Miscellaneous} *)
-val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
+(** If head is true, also allows applied global references. *)
+val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) ->
notation_key -> delimiters option -> GlobRef.t
(** Checks for already existing notations *)
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 98fa71e15d..03977fcb4e 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -62,15 +62,15 @@ let global_with_alias ?head qid =
try locate_global_with_alias ?head qid
with Not_found -> Nametab.error_global_not_found qid
-let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
+let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
| AN r ->
- global_with_alias ?head r
+ global_with_alias ~head r
| ByNotation (ntn,sc) ->
- Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)
+ Notation.interp_notation_as_global_reference ?loc ~head (fun _ -> true) ntn sc)
let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
| AN r ->
global_inductive_with_alias r
| ByNotation (ntn,sc) ->
destIndRef
- (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc))
+ (Notation.interp_notation_as_global_reference ?loc ~head:false isIndRef ntn sc))
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 1aa3af0087..53dc518bd3 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -14,7 +14,6 @@ open CAst
open Pattern
open Genredexpr
open Glob_term
-open Tacred
open Util
open Names
open Libnames
@@ -98,7 +97,7 @@ let intern_global_reference ist qid =
else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then
let id = qualid_basename qid in
ArgArg (qid.CAst.loc, GlobRef.VarRef id)
- else match locate_global_with_alias qid with
+ else match locate_global_with_alias ~head:true qid with
| r -> ArgArg (qid.CAst.loc, r)
| exception Not_found ->
if not !strict_check && qualid_is_ident qid then
@@ -294,45 +293,43 @@ let intern_destruction_arg ist = function
else
clear,ElimOnIdent (make ?loc id)
-let short_name = function
- | {v=AN qid} when qualid_is_ident qid && not !strict_check ->
+let short_name qid =
+ if qualid_is_ident qid && not !strict_check then
Some (make ?loc:qid.CAst.loc @@ qualid_basename qid)
- | _ -> None
-
-let intern_evaluable_global_reference ist qid =
- try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid)
- with Not_found ->
- if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid)
- else Nametab.error_global_not_found qid
-
-let intern_evaluable_reference_or_by_notation ist = function
- | {v=AN r} -> intern_evaluable_global_reference ist r
+ else None
+
+let evalref_of_globref ?loc ?short = function
+ | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short)
+ | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short)
+ | r ->
+ let tpe = match r with
+ | GlobRef.IndRef _ -> "inductive"
+ | GlobRef.ConstructRef _ -> "constructor"
+ | (GlobRef.VarRef _ | GlobRef.ConstRef _) -> assert false
+ in
+ user_err ?loc (str "Cannot turn" ++ spc () ++ str tpe ++ spc () ++
+ Nametab.pr_global_env Id.Set.empty r ++ spc () ++
+ str "into an evaluable reference.")
+
+let intern_evaluable ist = function
+ | {v=AN qid} ->
+ begin match intern_global_reference ist qid with
+ | ArgVar _ as v -> v
+ | ArgArg (loc, r) ->
+ let short = short_name qid in
+ evalref_of_globref ?loc ?short r
+ end
| {v=ByNotation (ntn,sc);loc} ->
- evaluable_of_global_reference ist.genv
- (Notation.interp_notation_as_global_reference ?loc
- GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
+ let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in
+ let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in
+ evalref_of_globref ?loc r
let intern_smart_global ist = function
| {v=AN r} -> intern_global_reference ist r
| {v=ByNotation (ntn,sc);loc} ->
- ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc
+ ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc ~head:true
GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc))
-(* Globalize a reduction expression *)
-let intern_evaluable ist r =
- let f ist r =
- let e = intern_evaluable_reference_or_by_notation ist r in
- let na = short_name r in
- ArgArg (e,na)
- in
- match r with
- | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist ->
- ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
- | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist ->
- let id = qualid_basename qid in
- ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id))
- | _ -> f ist r
-
let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
let intern_flag ist red =
@@ -393,10 +390,10 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let c = Constrintern.interp_reference sign r in
match DAst.get c with
| GRef (r,None) ->
- Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
+ Inl (evalref_of_globref r)
| GVar id ->
- let r = evaluable_of_global_reference ist.genv (GlobRef.VarRef id) in
- Inl (ArgArg (r,None))
+ let r = evalref_of_globref (GlobRef.VarRef id) in
+ Inl r
| _ ->
let bound_names = Glob_ops.bound_glob_vars c in
Inr (bound_names,(c,None),dummy_pat) in
diff --git a/test-suite/bugs/closed/bug_11727.v b/test-suite/bugs/closed/bug_11727.v
new file mode 100644
index 0000000000..d346f05c10
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11727.v
@@ -0,0 +1,8 @@
+Tactic Notation "myunfold" reference(x) := unfold x.
+Notation idnat := (@id nat).
+Goal let n := 0 in idnat n = 0.
+Proof.
+ intro n.
+ myunfold idnat.
+ myunfold n.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4925.v b/test-suite/bugs/closed/bug_4925.v
new file mode 100644
index 0000000000..d4e4b35351
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4925.v
@@ -0,0 +1,6 @@
+Axiom a: bool.
+
+Goal a = true.
+Proof.
+try unfold a.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5159.v b/test-suite/bugs/closed/bug_5159.v
new file mode 100644
index 0000000000..cbc924c2d3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5159.v
@@ -0,0 +1,12 @@
+Axiom foo : Type.
+Definition bar := 1.
+Definition bar' := Eval cbv -[bar] in bar.
+Declare Reduction red' := cbv -[bar].
+Opaque bar.
+Definition bar'' := Eval red' in bar.
+Declare Reduction red'' := cbv -[bar]. (* Error: Cannot coerce bar to an
+evaluable reference. *)
+Definition bar''' := Eval cbv -[bar] in bar. (* Error: Cannot coerce bar to an
+evaluable reference. *)
+Definition foo' := Eval cbv -[foo] in foo. (* Error: Cannot coerce foo to an
+evaluable reference. *)
diff --git a/test-suite/bugs/closed/bug_5764.v b/test-suite/bugs/closed/bug_5764.v
new file mode 100644
index 0000000000..0b015d9c7e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5764.v
@@ -0,0 +1,7 @@
+Module Type A.
+Parameter a : nat.
+End A.
+
+Module B (mA : A).
+Ltac cbv_a := cbv [mA.a].
+End B.
diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v
index 077b57c87f..6f0833211e 100644
--- a/test-suite/success/with_strategy.v
+++ b/test-suite/success/with_strategy.v
@@ -195,8 +195,8 @@ Opaque F.id.
Goal F.id 0 = F.id 0.
Fail unfold F.id.
- (* This should work, but it fails with "Cannot coerce F.id to an evaluable reference." *)
- Fail F.with_transparent_id ltac:(progress unfold F.id).
+ F.with_transparent_id ltac:(progress unfold F.id).
+ Undo.
F.with_transparent_id ltac:(let x := constr:(@F.id) in progress unfold x).
Abort.
@@ -212,8 +212,8 @@ Opaque F2.id.
Goal F2.id 0 = F2.id 0.
Fail unfold F2.id.
- (* This should work, but it fails with "Cannot coerce F2.id to an evaluable reference." *)
- Fail F2.with_transparent_id ltac:(progress unfold F2.id).
+ F2.with_transparent_id ltac:(progress unfold F2.id).
+ Undo.
F2.with_transparent_id ltac:(let x := constr:(@F2.id) in progress unfold x).
Abort.
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index a7170c8e18..faf53d3fad 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -906,7 +906,7 @@ let print_name env sigma na udecl =
match na with
| {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
print_any_name env sigma
- (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+ (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true)
ntn sc))
udecl
| {loc; v=Constrexpr.AN ref} ->
@@ -960,7 +960,7 @@ let print_about env sigma na udecl =
match na with
| {loc;v=Constrexpr.ByNotation (ntn,sc)} ->
print_about_any ?loc env sigma
- (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+ (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true)
ntn sc)) udecl
| {loc;v=Constrexpr.AN ref} ->
print_about_any ?loc env sigma (locate_any_name ref) udecl
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6568d7bf14..09201d727d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1785,7 +1785,7 @@ let interp_search_about_item env sigma =
try
let ref =
Notation.interp_notation_as_global_reference
- (fun _ -> true) s sc in
+ ~head:false (fun _ -> true) s sc in
GlobSearchSubPattern (Pattern.PRef ref)
with UserError _ ->
user_err ~hdr:"interp_search_about_item"
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:43:46 +0000