diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2quote.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2quote.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 |