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

3 files changed, 18 insertions, 3 deletions

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