diff options
author | 2012-01-12 16:08:29 +0100 | |
---|---|---|
committer | 2012-01-12 16:08:29 +0100 | |
commit | 23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch) | |
tree | f1ca9ba9240b98b8695a9f1870e56602734cf97c /parsing/ppconstr.mli | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) |
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
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. *) |