Merge PR #12698: Fixing mention of `unfold` as example of tactic taking a qualid in tactic notations

Reviewed-by: Zimmi48
Ack-by: jfehrle

2 files changed, 72 insertions, 4 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index fcd5ecc070..18149a690a 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1786,13 +1786,13 @@ Tactic notations allow customizing the syntax of tactics.
 
       * - ``reference``
         - :token:`qualid`
-        - a global reference of term
-        - :tacn:`unfold`
+        - a qualified identifier
+        - name of an |Ltac|-defined tactic
 
       * - ``smart_global``
         - :token:`reference`
         - a global reference of term
-        - :tacn:`with_strategy`
+        - :tacn:`unfold`, :tacn:`with_strategy`
 
       * - ``constr``
         - :token:`term`
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 7af09585d0..712cb6a135 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -15,6 +15,7 @@ Goal EQ nat 0 0.
 Hint Unfold EQ.
 auto.
 Qed.
+End toto.
 
 (* Check regular failure when statically existing ref does not exist
    any longer at run time *)
@@ -23,4 +24,71 @@ Goal let x := 0 in True.
 intro x.
 Fail (clear x; unfold x).
 Abort.
-End toto.
+
+(* Static analysis of unfold *)
+
+Module A.
+
+Opaque id.
+Ltac f := unfold id.
+Goal id 0 = 0.
+Fail f.
+Transparent id.
+f.
+Abort.
+
+End A.
+
+Module B.
+
+Module Type T. Axiom n : nat. End T.
+
+Module F(X:T).
+Ltac f := unfold X.n.
+End F.
+
+Module M. Definition n := 0. End M.
+Module N := F M.
+Goal match M.n with 0 => 0 | S _ => 1 end = 0.
+N.f.
+match goal with |- 0=0 => idtac end.
+Abort.
+
+End B.
+
+Module C.
+
+(* We reject inductive types and constructors *)
+
+Fail Ltac g := unfold nat.
+Fail Ltac g := unfold S.
+
+End C.
+
+Module D.
+
+(* In interactive mode, we delay the interpretation of short names *)
+
+Notation x := Nat.add.
+
+Goal let x := 0 in x = 0+0.
+unfold x.
+match goal with |- 0 = 0 => idtac end.
+Abort.
+
+Goal let x := 0 in x = 0+0.
+intro; unfold x. (* dynamic binding (but is it really the most natural?) *)
+match goal with |- 0 = 0+0 => idtac end.
+Abort.
+
+Goal let fst := 0 in fst = Datatypes.fst (0,0).
+unfold fst.
+match goal with |- 0 = 0 => idtac end.
+Abort.
+
+Goal let fst := 0 in fst = Datatypes.fst (0,0).
+intro; unfold fst. (* dynamic binding *)
+match goal with |- 0 = Datatypes.fst (0,0) => idtac end.
+Abort.
+
+End D.