From 6dc94fe5c1e02fccefbfedfcb1d4347274f3de0b Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 28 May 2001 12:14:49 +0000
Subject: Pretty -> Prettyp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pretty.mli | 59 ------------------------------------------------------
 1 file changed, 59 deletions(-)
 delete mode 100644 parsing/pretty.mli

(limited to 'parsing/pretty.mli')

diff --git a/parsing/pretty.mli b/parsing/pretty.mli
deleted file mode 100644
index b84c566348..0000000000
--- a/parsing/pretty.mli
+++ /dev/null
@@ -1,59 +0,0 @@
-(***********************************************************************)
-(*  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
-
-- 
cgit v1.2.3