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 cb2e406571..ddb39326d1 100644 --- a/src/tac2quote.mli +++ b/src/tac2quote.mli @@ -41,6 +41,8 @@ val of_intro_pattern : intro_pattern -> raw_tacexpr val of_intro_patterns : intro_pattern list located -> raw_tacexpr +val of_clause : ?loc:Loc.t -> clause -> raw_tacexpr + val of_induction_clause : induction_clause -> raw_tacexpr val of_rewriting : rewriting -> raw_tacexpr |