aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/04-tactics/10318-select-only-error.rst4
-rw-r--r--doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst5
-rw-r--r--doc/sphinx/proof-engine/ltac2.rst7
-rw-r--r--engine/proofview.ml42
-rw-r--r--proofs/refine.ml3
-rw-r--r--proofs/refine.mli3
-rw-r--r--proofs/refiner.ml55
-rw-r--r--proofs/refiner.mli29
-rw-r--r--proofs/tacmach.ml9
-rw-r--r--proofs/tacmach.mli4
-rw-r--r--tactics/tacticals.ml8
-rw-r--r--tactics/tacticals.mli9
-rw-r--r--test-suite/ltac2/notations.v24
-rw-r--r--test-suite/success/goal_selector.v8
-rw-r--r--user-contrib/Ltac2/tac2core.ml11
-rw-r--r--user-contrib/Ltac2/tac2quote.ml8
-rw-r--r--user-contrib/Ltac2/tac2quote.mli2
17 files changed, 80 insertions, 151 deletions
diff --git a/doc/changelog/04-tactics/10318-select-only-error.rst b/doc/changelog/04-tactics/10318-select-only-error.rst
new file mode 100644
index 0000000000..03ed15d948
--- /dev/null
+++ b/doc/changelog/04-tactics/10318-select-only-error.rst
@@ -0,0 +1,4 @@
+- The goal selector tactical ``only`` now checks that the goal range
+ it is given is valid instead of ignoring goals out of the focus
+ range. (`#10318 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan
+ Gilbert).
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/engine/proofview.ml b/engine/proofview.ml
index c00c90e5e9..d4f6fe3aef 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -373,32 +373,24 @@ let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t =
let open Proof in
Comb.get >>= fun comb ->
- let n = CList.length comb in
- (* First, remove empty intervals, and bound the intervals to the number
- of goals. *)
- let sanitize (i, j) =
- if i > j then None
- else if i > n then None
- else if j < 1 then None
- else Some ((max i 1), (min j n))
- in
- let l = CList.map_filter sanitize l in
+ let n = CList.length comb in
+ let ok (i, j) = 1 <= i && i <= j && j <= n in
+ if not (CList.for_all ok l) then nosuchgoal
+ else
match l with
- | [] -> nosuchgoal
- | (mi, _) :: _ ->
- (* Get the left-most goal to focus. This goal won't move, and we
- will then place all the other goals to focus to the right. *)
- let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in
- (* [CList.goto] returns a zipper, so that
- [(rev left) @ sub_right = comb]. *)
- let left, sub_right = CList.goto (mi-1) comb in
- let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in
- let sub, right = CList.partitioni p sub_right in
- let mj = mi - 1 + CList.length sub in
- Comb.set (CList.rev_append left (sub @ right)) >>
- tclFOCUS mi mj t
-
-
+ | [] -> nosuchgoal
+ | (mi, _) :: _ ->
+ (* Get the left-most goal to focus. This goal won't move, and we
+ will then place all the other goals to focus to the right. *)
+ let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in
+ (* [CList.goto] returns a zipper, so that
+ [(rev left) @ sub_right = comb]. *)
+ let left, sub_right = CList.goto (mi-1) comb in
+ let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in
+ let sub, right = CList.partitioni p sub_right in
+ let mj = mi - 1 + CList.length sub in
+ Comb.set (CList.rev_append left (sub @ right)) >>
+ tclFOCUS mi mj t
(** Like {!tclFOCUS} but selects a single goal by name. *)
let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 4a9404aa96..8439156e65 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -116,9 +116,6 @@ let lift c =
let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl
-let refine_one ~typecheck f =
- Proofview.Goal.enter_one (make_refine_enter ~typecheck f)
-
let refine ~typecheck f =
let f evd =
let (evd,c) = f evd in (evd,((), c))
diff --git a/proofs/refine.mli b/proofs/refine.mli
index b8948a92f3..93fd9d7a64 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -27,9 +27,6 @@ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> uni
raised during the interpretation of [t] are caught and result in
tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
-val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic
-(** A variant of [refine] which assumes exactly one goal under focus *)
-
val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
Proofview.Goal.t -> 'a tactic
(** The general version of refine. *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 799f4a380b..557f428be9 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -129,9 +129,6 @@ let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci
let tclTHEN_i tac taci gls =
finish_tac (thensi_tac taci (then_tac tac (start_tac gls)))
-let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci
-let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC
-
(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
[tac2] to every resulting subgoals *)
let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||]
@@ -253,46 +250,9 @@ let rec tclFIRST = function
| [] -> tclFAIL_s "No applicable tactic."
| t::rest -> tclORELSE0 t (tclFIRST rest)
-let ite_gen tcal tac_if continue tac_else gl=
- let success=ref false in
- let tac_if0 gl=
- let result=tac_if gl in
- success:=true;result in
- let tac_else0 e gl=
- if !success then
- iraise e
- else
- try
- tac_else gl
- with
- e' when CErrors.noncritical e' -> iraise e in
- try
- tcal tac_if0 continue gl
- with (* Breakpoint *)
- | e when CErrors.noncritical e ->
- let e = CErrors.push e in catch_failerror e; tac_else0 e gl
-
-(* Try the first tactic and, if it succeeds, continue with
- the second one, and if it fails, use the third one *)
-
-let tclIFTHENELSE=ite_gen tclTHEN
-
-(* Idem with tclTHENS and tclTHENSV *)
-
-let tclIFTHENSELSE=ite_gen tclTHENS
-
-let tclIFTHENSVELSE=ite_gen tclTHENSV
-
-let tclIFTHENTRYELSEMUST tac1 tac2 gl =
- tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl
-
(* Fails if a tactic did not solve the goal *)
let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
-(* Try the first that solves the current goal *)
-let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
-
-
(* Iteration tacticals *)
let tclDO n t =
@@ -311,22 +271,7 @@ let rec tclREPEAT t g =
let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
-(* Repeat on the first subgoal (no failure if no more subgoal) *)
-let rec tclREPEAT_MAIN t g =
- (tclORELSE (tclTHEN_i t (fun i -> if Int.equal i 1 then (tclREPEAT_MAIN t) else
- tclIDTAC)) tclIDTAC) g
-
(* Change evars *)
let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
-
-let tclEVARUNIVCONTEXT ctx gls = tclIDTAC {gls with sigma= Evd.set_universe_context gls.sigma ctx}
-
-(* Push universe context *)
-let tclPUSHCONTEXT rigid ctx tac gl =
- tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl
-
let tclPUSHEVARUNIVCONTEXT ctx gl =
tclEVARS (Evd.merge_universe_context (project gl) ctx) gl
-
-let tclPUSHCONSTRAINTS cst gl =
- tclEVARS (Evd.add_constraints (project gl) cst) gl
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 52cbf7658b..0f34a79c49 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -32,12 +32,8 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic
(** [tclEVARS sigma] changes the current evar map *)
val tclEVARS : evar_map -> tactic
-val tclEVARUNIVCONTEXT : UState.t -> tactic
-
-val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic
val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic
-val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic
(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
[tac2] to every resulting subgoals *)
@@ -86,16 +82,6 @@ val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
[tac2] for the remaining last subgoals (previously called tclTHENST) *)
val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
-(** [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
- applies [t1],...,[tn] on the last [n] resulting subgoals and leaves
- unchanged the other subgoals *)
-val tclTHENLASTn : tactic -> tactic array -> tactic
-
-(** [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
- applies [t1],...,[tn] on the first [n] resulting subgoals and leaves
- unchanged the other subgoals (previously called [tclTHENSI]) *)
-val tclTHENFIRSTn : tactic -> tactic array -> tactic
-
(** A special exception for levels for the Fail tactic *)
exception FailError of int * Pp.t Lazy.t
@@ -106,9 +92,7 @@ val catch_failerror : Exninfo.iexn -> unit
val tclORELSE0 : tactic -> tactic -> tactic
val tclORELSE : tactic -> tactic -> tactic
val tclREPEAT : tactic -> tactic
-val tclREPEAT_MAIN : tactic -> tactic
val tclFIRST : tactic list -> tactic
-val tclSOLVE : tactic list -> tactic
val tclTRY : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclCOMPLETE : tactic -> tactic
@@ -118,16 +102,3 @@ val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclSHOWHYPS : tactic -> tactic
-
-(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
- if it succeeds, applies [tac2] to the resulting subgoals,
- and if not applies [tac3] to the initial goal [gls] *)
-val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
-val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic
-val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic
-
-(** [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1]
- has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed.
- Equivalent to [(tac1;try tac2)||tac2] *)
-
-val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 93031c2202..d7b4f729cb 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -81,12 +81,10 @@ let pf_type_of = pf_reduce type_of
let pf_get_type_of = pf_reduce Retyping.get_type_of
let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV
-let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL
let pf_const_value = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c))
let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind
-
let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls
(* Pretty-printers *)
@@ -181,14 +179,7 @@ module New = struct
let pf_hnf_type_of gl t =
pf_whd_all gl (pf_get_type_of gl t)
- let pf_whd_all gl t = pf_apply whd_all gl t
let pf_compute gl t = pf_apply compute gl t
let pf_nf_evar gl t = nf_evar (project gl) t
-
- let pf_undefined_evars gl =
- let sigma = Proofview.Goal.sigma gl in
- let ev = Proofview.Goal.goal gl in
- let evi = Evd.find sigma ev in
- Evarutil.filtered_undefined_evars_of_evar_info sigma evi
end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 23e1e6f566..195be04986 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -64,7 +64,6 @@ val pf_unfoldn : (occurrences * evaluable_global_reference) list
val pf_const_value : Goal.goal sigma -> pconstant -> constr
val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool
-val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool
(** {6 Pretty-printing functions (debug only). } *)
val pr_gls : Goal.goal sigma -> Pp.t
@@ -109,11 +108,8 @@ module New : sig
val pf_hnf_constr : Proofview.Goal.t -> constr -> types
val pf_hnf_type_of : Proofview.Goal.t -> constr -> types
- val pf_whd_all : Proofview.Goal.t -> constr -> constr
val pf_compute : Proofview.Goal.t -> constr -> constr
val pf_nf_evar : Proofview.Goal.t -> constr -> constr
- (** Gathers the undefined evars of the given goal. *)
- val pf_undefined_evars : Proofview.Goal.t -> Evar.Set.t
end
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 59fd8b37d6..81700986ea 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -43,12 +43,8 @@ let tclTHENS = Refiner.tclTHENS
let tclTHENSV = Refiner.tclTHENSV
let tclTHENSFIRSTn = Refiner.tclTHENSFIRSTn
let tclTHENSLASTn = Refiner.tclTHENSLASTn
-let tclTHENFIRSTn = Refiner.tclTHENFIRSTn
-let tclTHENLASTn = Refiner.tclTHENLASTn
let tclREPEAT = Refiner.tclREPEAT
-let tclREPEAT_MAIN = Refiner.tclREPEAT_MAIN
let tclFIRST = Refiner.tclFIRST
-let tclSOLVE = Refiner.tclSOLVE
let tclTRY = Refiner.tclTRY
let tclCOMPLETE = Refiner.tclCOMPLETE
let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
@@ -58,10 +54,6 @@ let tclDO = Refiner.tclDO
let tclPROGRESS = Refiner.tclPROGRESS
let tclSHOWHYPS = Refiner.tclSHOWHYPS
let tclTHENTRY = Refiner.tclTHENTRY
-let tclIFTHENELSE = Refiner.tclIFTHENELSE
-let tclIFTHENSELSE = Refiner.tclIFTHENSELSE
-let tclIFTHENSVELSE = Refiner.tclIFTHENSVELSE
-let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST
(************************************************************************)
(* Tacticals applying on hypotheses *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 201b7801c3..a9ccda527f 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -31,13 +31,9 @@ val tclTHENLAST : tactic -> tactic -> tactic
val tclTHENS : tactic -> tactic list -> tactic
val tclTHENSV : tactic -> tactic array -> tactic
val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
-val tclTHENLASTn : tactic -> tactic array -> tactic
val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
-val tclTHENFIRSTn : tactic -> tactic array -> tactic
val tclREPEAT : tactic -> tactic
-val tclREPEAT_MAIN : tactic -> tactic
val tclFIRST : tactic list -> tactic
-val tclSOLVE : tactic list -> tactic
val tclTRY : tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
@@ -49,11 +45,6 @@ val tclSHOWHYPS : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclMAP : ('a -> tactic) -> 'a list -> tactic
-val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
-val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic
-val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic
-val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
-
(** {6 Tacticals applying to hypotheses } *)
val onNthHypId : int -> (Id.t -> tactic) -> tactic
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/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
index 0951c5c8d4..ae834e7696 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -13,13 +13,15 @@ Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true.
Proof.
do 2 dup.
- repeat split.
- 2, 4-99, 100-3:idtac.
+ Fail 7:idtac.
+ Fail 2-1:idtac.
+ 1,2,4-6:idtac.
2-5:exact One.
par:exact Zero.
- repeat split.
3-6:swap 1 4.
1-5:swap 1 5.
- 0-4:exact One.
+ 1-4:exact One.
all:exact Zero.
- repeat split.
1, 3:exact Zero.
@@ -34,7 +36,7 @@ Qed.
Goal True -> True.
Proof.
- intros y; only 1-2 : repeat idtac.
+ intros y.
1-1:match goal with y : _ |- _ => let x := y in idtac x end.
Fail 1-1:let x := y in idtac x.
1:let x := y in idtac x.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 12:47:27 +0000