diff options
Diffstat (limited to 'src/tac2quote.mli')
| -rw-r--r-- | src/tac2quote.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/tac2quote.mli b/src/tac2quote.mli index 9f42c60042..ccb832535a 100644 --- a/src/tac2quote.mli +++ b/src/tac2quote.mli @@ -75,6 +75,8 @@ val of_dispatch : dispatch -> raw_tacexpr val of_strategy_flag : strategy_flag -> raw_tacexpr +val of_pose : pose -> raw_tacexpr + val of_constr_matching : constr_matching -> raw_tacexpr (** {5 Generic arguments} *) |