1 files changed, 11 insertions, 7 deletions
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 =