Allow scope delimiters in Ltac2 open_constr:(...) quotation.

Fixes #12806: Ltac2 Notation's open_constr should accept scope stacks.

3 files changed, 22 insertions, 9 deletions

diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 948a359124..c299562194 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1679,6 +1679,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)
@@ -1707,7 +1717,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