diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-28 12:14:49 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-28 12:14:49 +0000 |
commit | 6dc94fe5c1e02fccefbfedfcb1d4347274f3de0b (patch) | |
tree | 4a33333de304fb331f0f7b2b9ea761a8301b2f8d /parsing/prettyp.mli | |
parent | 47bde1826b6329650f8546ac1fca1f2e90d85fcb (diff) |
Pretty -> Prettyp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/prettyp.mli')
-rw-r--r-- | parsing/prettyp.mli | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli new file mode 100644 index 000000000..b84c56634 --- /dev/null +++ b/parsing/prettyp.mli @@ -0,0 +1,59 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(*i*) +open Pp +open Names +open Sign +open Term +open Inductive +open Reduction +open Environ +(*i*) + +(* A Pretty-Printer for the Calculus of Inductive Constructions. *) + +val assumptions_for_print : name list -> names_context + +val print_closed_sections : bool ref +val print_impl_args : int list -> std_ppcmds +val print_context : bool -> Lib.library_segment -> std_ppcmds +val print_library_entry : bool -> (section_path * Lib.node) -> std_ppcmds +val print_full_context : unit -> std_ppcmds +val print_full_context_typ : unit -> std_ppcmds +val print_sec_context : Nametab.qualid -> std_ppcmds +val print_sec_context_typ : Nametab.qualid -> std_ppcmds +val print_judgment : env -> unsafe_judgment -> std_ppcmds +val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds +val print_eval : + 'a reduction_function -> env -> unsafe_judgment -> std_ppcmds +(* This function is exported for the graphical user-interface pcoq *) +val build_inductive : section_path -> int -> + global_reference * rel_context * types * identifier array * types array +val print_mutual : section_path -> std_ppcmds +val print_name : Nametab.qualid -> std_ppcmds +val print_opaque_name : Nametab.qualid -> std_ppcmds +val print_local_context : unit -> std_ppcmds + +(*i +val print_extracted_name : identifier -> std_ppcmds +val print_extraction : unit -> std_ppcmds +val print_extracted_vars : unit -> std_ppcmds +i*) + +(* Pretty-printing functions for classes and coercions *) +val print_graph : unit -> std_ppcmds +val print_classes : unit -> std_ppcmds +val print_coercions : unit -> std_ppcmds +val print_path_between : identifier -> identifier -> std_ppcmds + + +val inspect : int -> std_ppcmds + |