diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-12 17:49:21 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-12 17:49:21 +0000 |
commit | cb1ae314411d78952062e5092804b85d981ad6e1 (patch) | |
tree | 52b9a4058c89b5849d875a4c1129951f35e9c1b1 /translate/ppconstrnew.mli | |
parent | 7cb6a61133b6e3c2cd5601282a1f472ff0104c1f (diff) |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate/ppconstrnew.mli')
-rw-r--r-- | translate/ppconstrnew.mli | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli index 1488a9d17..27e1307c5 100644 --- a/translate/ppconstrnew.mli +++ b/translate/ppconstrnew.mli @@ -20,22 +20,29 @@ open Topconstr open Names open Util +val prec_less : int -> int * Ppextend.parenRelation -> bool + val split_fix : int -> constr_expr -> constr_expr -> (name located list * constr_expr) list * constr_expr * constr_expr -val pr_global : global_reference -> std_ppcmds - -val gentermpr : Coqast.t -> std_ppcmds -val gentermpr_core : bool -> env -> constr -> std_ppcmds +val pr_global : Idset.t -> global_reference -> std_ppcmds val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds val pr_name : name -> std_ppcmds val pr_qualid : qualid -> std_ppcmds val pr_red_expr : - ('a -> std_ppcmds) * ('b -> std_ppcmds) -> + ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) -> ('a,'b) red_expr_gen -> std_ppcmds - + val pr_sort : rawsort -> std_ppcmds val pr_pattern : Tacexpr.pattern_expr -> std_ppcmds val pr_constr : constr_expr -> std_ppcmds -val pr_may_eval : ('a -> std_ppcmds) -> 'a may_eval -> std_ppcmds +val pr_lconstr : constr_expr -> std_ppcmds +val pr_constr_env : env -> constr_expr -> std_ppcmds +val pr_lconstr_env : env -> constr_expr -> std_ppcmds +val pr_cases_pattern : cases_pattern_expr -> std_ppcmds +val pr_binders : (name located list * constr_expr) list -> std_ppcmds +val pr_may_eval : + ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a may_eval -> std_ppcmds +val pr_metanum : ('a -> std_ppcmds) -> 'a or_metanum -> std_ppcmds +val pr_metaid : identifier -> std_ppcmds |