diff options
Diffstat (limited to 'parsing/ppconstr.mli')
-rw-r--r-- | parsing/ppconstr.mli | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index d27b318a..7a24eb9f 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -1,19 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ppconstr.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Pp open Environ open Term open Libnames open Pcoq -open Rawterm +open Glob_term open Topconstr open Names open Util @@ -23,9 +21,6 @@ val extract_lam_binders : constr_expr -> local_binder list * constr_expr val extract_prod_binders : constr_expr -> local_binder list * constr_expr -val extract_def_binders : - constr_expr -> constr_expr -> - local_binder list * constr_expr * constr_expr val split_fix : int -> constr_expr -> constr_expr -> local_binder list * constr_expr * constr_expr @@ -56,12 +51,16 @@ val pr_with_occurrences : ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds val pr_red_expr : ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) -> - ('a,'b,'c) red_expr_gen -> std_ppcmds + ('a,'b,'c) red_expr_gen -> std_ppcmds val pr_may_eval : ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('c -> std_ppcmds) -> ('a,'b,'c) may_eval -> std_ppcmds -val pr_rawsort : rawsort -> std_ppcmds +val pr_glob_sort : glob_sort -> std_ppcmds +val pr_guard_annot : (constr_expr -> std_ppcmds) -> + local_binder list -> + ('a * Names.identifier) option * recursion_order_expr -> + std_ppcmds val pr_binders : local_binder list -> std_ppcmds val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds @@ -80,22 +79,23 @@ type term_pr = { val set_term_pr : term_pr -> unit val default_term_pr : term_pr -(* The modular constr printer. +(** The modular constr printer. [modular_constr_pr pr s p t] prints the head of the term [t] and calls [pr] on its subterms. - [s] is typically {!Pp.mt} and [p] is [lsimple] for "constr" printers and [ltop] - for "lconstr" printers (spiwack: we might need more specification here). + [s] is typically {!Pp.mt} and [p] is [lsimpleconstr] for "constr" printers + and [ltop] for "lconstr" printers (spiwack: we might need more + specification here). We can make a new modular constr printer by overriding certain branches, for instance if we want to build a printer which prints "Prop" as "Omega" instead we can proceed as follows: let my_modular_constr_pr pr s p = function - | CSort (_,RProp Null) -> str "Omega" + | CSort (_,GProp Null) -> str "Omega" | t -> modular_constr_pr pr s p t Which has the same type. We can turn a modular printer into a printer by taking its fixpoint. *) type precedence -val lsimple : precedence +val lsimpleconstr : precedence val ltop : precedence val modular_constr_pr : ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) -> |