[Ltac2] Interpretation scopes in “constr” arguments of tactic notations

6 files changed, 54 insertions, 3 deletions

diff --git a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst
new file mode 100644
index 0000000000..bd1c0c42e8
--- /dev/null
+++ b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst
@@ -0,0 +1,5 @@
+- Ltac2 tactic notations with “constr” arguments can specify the
+  interpretation scope for these arguments;
+  see :ref:`ltac2_notations` for details
+  (`#10289 <https://github.com/coq/coq/pull/10289>`_,
+  by Vincent Laporte).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 5f2e911ff9..36eeff6192 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -655,6 +655,8 @@ this features has the same semantics as in Ltac1. In particular, a ``reverse``
 flag can be specified to match hypotheses from the more recently introduced to
 the least recently introduced one.
 
+.. _ltac2_notations:
+
 Notations
 ---------
 
@@ -679,6 +681,11 @@ The following scopes are built-in.
 
   + parses :n:`c = @term` and produces :n:`constr:(c)`
 
+  This scope can be parameterized by a list of delimiting keys of interpretation
+  scopes (as described in :ref:`LocalInterpretationRulesForNotations`),
+  describing how to interpret the parsed term. For instance, :n:`constr(A, B)`
+  parses :n:`c = @term` and produces :n:`constr:(c%A%B)`.
+
 - :n:`ident`:
 
   + parses :n:`id = @ident` and produces :n:`ident:(id)`
diff --git a/test-suite/ltac2/notations.v b/test-suite/ltac2/notations.v
new file mode 100644
index 0000000000..3d2a875e38
--- /dev/null
+++ b/test-suite/ltac2/notations.v
@@ -0,0 +1,24 @@
+From Ltac2 Require Import Ltac2.
+From Coq Require Import ZArith String List.
+
+Open Scope Z_scope.
+
+Check 1 + 1 : Z.
+
+Ltac2 Notation "ex" arg(constr(nat,Z)) := arg.
+
+Check (1 + 1)%nat%Z = 1%nat.
+
+Lemma two : nat.
+  refine (ex (1 + 1)).
+Qed.
+
+Import ListNotations.
+Close Scope list_scope.
+
+Ltac2 Notation "sl" arg(constr(string,list)) := arg.
+
+Lemma maybe : list bool.
+Proof.
+  refine (sl ["left" =? "right"]).
+Qed.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index da8600109e..e2bab96e20 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1355,6 +1355,16 @@ let () = add_scope "thunk" begin function
 | arg -> scope_fail "thunk" arg
 end
 
+let () = add_scope "constr" (fun arg ->
+    let delimiters = List.map (function
+        | SexprRec (_, { v = Some s }, []) -> s
+        | _ -> scope_fail "constr" arg)
+        arg
+    in
+    let act e = Tac2quote.of_constr ~delimiters e in
+    Tac2entries.ScopeRule (Extend.Aentry Pcoq.Constr.constr, act)
+  )
+
 let add_expr_scope name entry f =
   add_scope name begin function
   | [] -> Tac2entries.ScopeRule (Extend.Aentry entry, f)
@@ -1382,7 +1392,6 @@ let () = add_expr_scope "assert" q_assert Tac2quote.of_assertion
 let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_matching
 let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_matching
 
-let () = add_generic_scope "constr" Pcoq.Constr.constr Tac2quote.wit_constr
 let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr
 let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
 
diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml
index a98264745e..81442c9d6b 100644
--- a/user-contrib/Ltac2/tac2quote.ml
+++ b/user-contrib/Ltac2/tac2quote.ml
@@ -94,8 +94,14 @@ let of_anti f = function
 
 let of_ident {loc;v=id} = inj_wit ?loc wit_ident id
 
-let of_constr c =
+let of_constr ?delimiters c =
   let loc = Constrexpr_ops.constr_loc c in
+  let c = Option.cata
+      (List.fold_left (fun c d ->
+           CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c))
+          c)
+      c delimiters
+  in
   inj_wit ?loc wit_constr c
 
 let of_open_constr c =
diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli
index 1b03dad8ec..1c859063aa 100644
--- a/user-contrib/Ltac2/tac2quote.mli
+++ b/user-contrib/Ltac2/tac2quote.mli
@@ -32,7 +32,7 @@ val of_variable : Id.t CAst.t -> raw_tacexpr
 
 val of_ident : Id.t CAst.t -> raw_tacexpr
 
-val of_constr : Constrexpr.constr_expr -> raw_tacexpr
+val of_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr
 
 val of_open_constr : Constrexpr.constr_expr -> raw_tacexpr