From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 parsing/ppconstr.mli | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

(limited to 'parsing/ppconstr.mli')

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. *)
-- 
cgit v1.2.3