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 403d333f38..3f6c9a55e5 100644 --- a/src/tac2quote.mli +++ b/src/tac2quote.mli @@ -51,6 +51,8 @@ val of_destruction_arg : destruction_arg -> raw_tacexpr val of_induction_clause : induction_clause -> raw_tacexpr +val of_conversion : conversion -> raw_tacexpr + val of_rewriting : rewriting -> raw_tacexpr val of_occurrences : occurrences -> raw_tacexpr |