diff options
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli index a444bb5371..94588f1dfa 100644 --- a/translate/ppvernacnew.mli +++ b/translate/ppvernacnew.mli @@ -29,3 +29,6 @@ open Topconstr val sep_end : unit -> std_ppcmds val pr_vernac : vernac_expr -> std_ppcmds + +val pr_vernac_solve : + int * Environ.env * Tacexpr.glob_tactic_expr * bool -> std_ppcmds |