diff options
Diffstat (limited to 'parsing/ppconstr.mli')
| -rw-r--r-- | parsing/ppconstr.mli | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli new file mode 100644 index 000000000..d9b8b6ea5 --- /dev/null +++ b/parsing/ppconstr.mli @@ -0,0 +1,33 @@ +(****************************************************************************) +(* *) +(* The Coq Proof Assistant *) +(* *) +(* Projet Coq *) +(* *) +(* INRIA LRI-CNRS ENS-CNRS *) +(* Rocquencourt Orsay Lyon *) +(* *) +(****************************************************************************) + +(* $Id$ *) + +open Pp +open Environ +open Term +open Nametab +open Pcoq +open Rawterm +open Extend + +val pr_global : global_reference -> std_ppcmds +val gentermpr : Coqast.t -> std_ppcmds +val gentermpr_core : bool -> env -> constr -> std_ppcmds + +val pr_qualid : qualid -> std_ppcmds +val pr_red_expr : + ('a -> std_ppcmds) * ('b -> std_ppcmds) -> + ('a,'b) red_expr_gen -> std_ppcmds + +val pr_pattern : Tacexpr.pattern_ast -> std_ppcmds +val pr_constr : Genarg.constr_ast -> std_ppcmds +val pr_may_eval : ('a -> std_ppcmds) -> 'a may_eval -> std_ppcmds |