diff options
Diffstat (limited to 'translate/pptacticnew.mli')
| -rw-r--r-- | translate/pptacticnew.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli index 4e8e29a53..b6861f816 100644 --- a/translate/pptacticnew.mli +++ b/translate/pptacticnew.mli @@ -15,6 +15,8 @@ open Proof_type open Topconstr open Names +val qsnew : string -> std_ppcmds + val pr_raw_tactic : Environ.env -> raw_tactic_expr -> std_ppcmds val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds |