diff options
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 |