diff options
Diffstat (limited to 'parsing/printer.mli')
| -rw-r--r-- | parsing/printer.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli index 0e25f1bd0d..338bff3b3a 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -91,6 +91,13 @@ val pr_rel_context : env -> rel_context -> std_ppcmds val pr_rel_context_of : env -> std_ppcmds val pr_context_of : env -> std_ppcmds +(* Predicates *) + +val pr_predicate : ('a -> std_ppcmds) -> (bool * 'a list) -> std_ppcmds +val pr_cpred : Cpred.t -> std_ppcmds +val pr_idpred : Idpred.t -> std_ppcmds +val pr_transparent_state : transparent_state -> std_ppcmds + (* Proofs *) val pr_goal : goal -> std_ppcmds |