Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.

Reviewed-by: JasonGross

6 files changed, 39 insertions, 11 deletions

diff --git a/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst
new file mode 100644
index 0000000000..9753ce915b
--- /dev/null
+++ b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Allow scope delimiters in Ltac2 open_constr:(...) quotation
+  (`#13939 <https://github.com/coq/coq/pull/13939>`_,
+  fixes `#12806 <https://github.com/coq/coq/issues/12806>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 294c56ef06..25ac72069b 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1375,8 +1375,9 @@ table further down lists the classes that that are handled plainly.
     the term (as described in  :ref:`LocalInterpretationRulesForNotations`).  The last
     :token:`scope_key` is the top of the scope stack that's applied to the :token:`term`.
 
-  :n:`open_constr`
-    Parses an open :token:`term`.
+  :n:`open_constr {? ( {+, @scope_key } ) }`
+    Parses an open :token:`term`. Like :n:`constr` above, this class
+    accepts a list of notation scopes with the same effects.
 
   :n:`ident`
     Parses :token:`ident` or :n:`$@ident`.  The first form returns :n:`ident:(@ident)`,
diff --git a/test-suite/bugs/closed/bug_12806.v b/test-suite/bugs/closed/bug_12806.v
new file mode 100644
index 0000000000..ee221d33a6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12806.v
@@ -0,0 +1,9 @@
+Require Import Ltac2.Ltac2.
+
+Declare Scope my_scope.
+Delimit Scope my_scope with my_scope.
+
+Notation "###" := tt : my_scope.
+
+Ltac2 Notation "bar" c(open_constr(my_scope)) := c.
+Ltac2 Eval bar ###.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 457b8e1acf..4758ecf5bd 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1754,6 +1754,16 @@ let () = add_scope "constr" (fun arg ->
     Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act)
   )
 
+let () = add_scope "open_constr" (fun arg ->
+    let delimiters = List.map (function
+        | SexprRec (_, { v = Some s }, []) -> s
+        | _ -> scope_fail "open_constr" arg)
+        arg
+    in
+    let act e = Tac2quote.of_open_constr ~delimiters e in
+    Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act)
+  )
+
 let add_expr_scope name entry f =
   add_scope name begin function
   | [] -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm entry, f)
@@ -1782,7 +1792,6 @@ let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_
 let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_matching
 let () = add_expr_scope "format" Pcoq.Prim.lstring Tac2quote.of_format
 
-let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr
 let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
 
 (** seq scope, a bit hairy *)
diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml
index d1a72fcfd1..2d65f9ec3e 100644
--- a/user-contrib/Ltac2/tac2quote.ml
+++ b/user-contrib/Ltac2/tac2quote.ml
@@ -102,18 +102,22 @@ let of_anti f = function
 
 let of_ident {loc;v=id} = inj_wit ?loc wit_ident id
 
+let quote_constr ?delimiters c =
+  let loc = Constrexpr_ops.constr_loc c in
+  Option.cata
+    (List.fold_left (fun c d ->
+          CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c))
+        c)
+    c delimiters
+
 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
+  let c = quote_constr ?delimiters c in
   inj_wit ?loc wit_constr c
 
-let of_open_constr c =
+let of_open_constr ?delimiters c =
   let loc = Constrexpr_ops.constr_loc c in
+  let c = quote_constr ?delimiters c in
   inj_wit ?loc wit_open_constr c
 
 let of_bool ?loc b =
diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli
index fcd1339cd7..6e2f548319 100644
--- a/user-contrib/Ltac2/tac2quote.mli
+++ b/user-contrib/Ltac2/tac2quote.mli
@@ -36,7 +36,7 @@ val of_ident : Id.t CAst.t -> raw_tacexpr
 
 val of_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr
 
-val of_open_constr : Constrexpr.constr_expr -> raw_tacexpr
+val of_open_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr
 
 val of_list : ?loc:Loc.t -> ('a -> raw_tacexpr) -> 'a list -> raw_tacexpr