diff options
Diffstat (limited to 'parsing/ppconstr.mli')
| -rw-r--r-- | parsing/ppconstr.mli | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index d27b318a..f9ed3af0 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-2010 *) (* \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 @@ -61,7 +56,7 @@ 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_binders : local_binder list -> std_ppcmds val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds @@ -80,7 +75,7 @@ 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] @@ -89,7 +84,7 @@ val default_term_pr : term_pr 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. *) |