From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 parsing/printer.mli | 112 +++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 76 insertions(+), 36 deletions(-)

(limited to 'parsing/printer.mli')

diff --git a/parsing/printer.mli b/parsing/printer.mli
index c44be124..66471d41 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: printer.mli,v 1.26.2.2 2005/01/21 16:42:37 herbelin Exp $ i*)
+(*i $Id: printer.mli 7855 2006-01-12 08:21:57Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -19,42 +19,82 @@ open Rawterm
 open Pattern
 open Nametab
 open Termops
+open Evd
+open Proof_type
+open Rawterm
 (*i*)
 
 (* These are the entry points for printing terms, context, tac, ... *)
-(*i
-val gentacpr  : Tacexpr.raw_tactic_expr -> std_ppcmds
-i*)
-
-val prterm_env      : env -> constr -> std_ppcmds
-val prterm_env_at_top : env -> constr -> std_ppcmds
-val prterm          : constr -> std_ppcmds
-val prtype_env      : env -> types -> std_ppcmds
-val prtype          : types -> std_ppcmds
-val prjudge_env     :
-  env -> Environ.unsafe_judgment -> std_ppcmds * std_ppcmds
-val prjudge         : Environ.unsafe_judgment -> std_ppcmds * std_ppcmds
-
-val pr_rawterm       : Rawterm.rawconstr -> std_ppcmds
-val pr_cases_pattern : Rawterm.cases_pattern -> std_ppcmds
-
-val pr_constant     : env -> constant -> std_ppcmds
-val pr_existential  : env -> existential -> std_ppcmds
-val pr_constructor  : env -> constructor -> std_ppcmds
-val pr_inductive    : env -> inductive -> std_ppcmds
-val pr_global       : global_reference -> std_ppcmds
-val pr_ref_label    : constr_label -> std_ppcmds
-val pr_pattern      : constr_pattern -> std_ppcmds
-val pr_pattern_env  : env -> names_context -> constr_pattern -> std_ppcmds
-
-val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds
-
-val pr_var_decl     : env -> named_declaration -> std_ppcmds
-val pr_rel_decl     : env -> rel_declaration -> std_ppcmds
-
-val pr_named_context_of : env -> std_ppcmds
-val pr_rel_context  : env -> rel_context -> std_ppcmds
-val pr_context_of   : env -> std_ppcmds
-
-val emacs_str       : string -> string
 
+(* Terms *)
+
+val pr_lconstr_env         : env -> constr -> std_ppcmds
+val pr_lconstr_env_at_top  : env -> constr -> std_ppcmds
+val pr_lconstr             : constr -> std_ppcmds
+
+val pr_constr_env          : env -> constr -> std_ppcmds
+val pr_constr              : constr -> std_ppcmds
+
+val pr_ltype_env           : env -> types -> std_ppcmds
+val pr_ltype               : types -> std_ppcmds
+
+val pr_type_env            : env -> types -> std_ppcmds
+val pr_type                : types -> std_ppcmds
+
+val pr_ljudge_env          : env -> unsafe_judgment -> std_ppcmds * std_ppcmds
+val pr_ljudge              : unsafe_judgment -> std_ppcmds * std_ppcmds
+
+val pr_lrawconstr_env      : env -> rawconstr -> std_ppcmds
+val pr_lrawconstr          : rawconstr -> std_ppcmds
+
+val pr_rawconstr_env       : env -> rawconstr -> std_ppcmds
+val pr_rawconstr           : rawconstr -> std_ppcmds
+
+val pr_constr_pattern_env  : env -> constr_pattern -> std_ppcmds
+val pr_constr_pattern      : constr_pattern -> std_ppcmds
+
+val pr_cases_pattern       : cases_pattern -> std_ppcmds
+
+(* Printing global references using names as short as possible *)
+
+val pr_global_env          : Idset.t -> global_reference -> std_ppcmds
+val pr_global              : global_reference -> std_ppcmds
+
+val pr_constant            : env -> constant -> std_ppcmds
+val pr_existential         : env -> existential -> std_ppcmds
+val pr_constructor         : env -> constructor -> std_ppcmds
+val pr_inductive           : env -> inductive -> std_ppcmds
+val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds
+
+(* Contexts *)
+
+val pr_ne_context_of       : std_ppcmds -> env -> std_ppcmds
+
+val pr_var_decl            : env -> named_declaration -> std_ppcmds
+val pr_rel_decl            : env -> rel_declaration -> std_ppcmds
+
+val pr_named_context       : env -> named_context -> std_ppcmds
+val pr_named_context_of    : env -> std_ppcmds
+val pr_rel_context         : env -> rel_context -> std_ppcmds
+val pr_rel_context_of      : env -> std_ppcmds
+val pr_context_of          : env -> std_ppcmds
+
+(* Proofs *)
+
+val pr_goal                : goal -> std_ppcmds
+val pr_subgoals            : evar_map -> goal list -> std_ppcmds
+val pr_subgoal             : int -> goal list -> std_ppcmds
+
+val pr_open_subgoals       : unit -> std_ppcmds
+val pr_nth_open_subgoal    : int -> std_ppcmds
+val pr_evars_int           : int -> (evar * evar_info) list -> std_ppcmds
+
+val pr_prim_rule           : prim_rule -> std_ppcmds
+
+(* Emacs/proof general support *)
+
+val emacs_str              : string -> string
+
+(* Backwards compatibility *)
+
+val prterm                 : constr -> std_ppcmds (* = pr_lconstr *)
-- 
cgit v1.2.3