From f3eaf2869e84c942d56a7fe0cc459d9943e4b059 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 18 Dec 2007 12:19:12 +0000
Subject: Nettoyage de code en vue de la release. Plus de Warning: Unused
 Variable, et plus de trucs useless qui traînaient par ma faute (y compris
 dans le noyau, la honte).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.ml | 40 ----------------------------------------
 1 file changed, 40 deletions(-)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index c153169ab4..46a44a9b2e 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -330,43 +330,3 @@ type inv_rel_key = int (* index in the [rel_context] part of environment
 
 type id_key = inv_rel_key tableKey
 
-
-
-(* spiwack : internal representation printing *)
-
-let string_of_identifier id = id
-let string_of_module_ident id = id
-let string_of_label lbl = lbl (* not public *)
-let string_of_dir_path path = "["^String.concat "; " (List.map string_of_module_ident path)^"]"
-let string_of_name =
-  function
-  | Name id -> "Name "^id
-  | Anonymous -> "Anonymous"
-
-let rec string_of_module_path = (* not public *)
-  function
-  | MPfile path -> "MPfile "^string_of_dir_path path
-  | MPbound _ -> "MPbound "^"?" (*of mod_bound_id*)
-  | MPself _ -> "MPself "^"?" (* of mod_self_id *)
-  | MPdot (mpath, lbl) -> 
-         "MPdot ("^string_of_module_path mpath^", "^string_of_label lbl^")"
-          (* of module_path * label *)
-
-let string_of_kernel_name = (* not public *)
-   function
-   |(mpath, path, lbl) -> 
-         "("^string_of_module_path mpath^", "^
-             string_of_dir_path path^", "^
-             string_of_label lbl ^")"
-
-let string_of_constant = string_of_kernel_name
-let string_of_mutual_inductive = string_of_kernel_name
-let string_of_inductive = 
-   function
-   | (mind, i) -> "("^string_of_mutual_inductive mind^", "^string_of_int i^")"
-let string_of_constructor =
-   function
-   | (ind, i) -> "("^string_of_inductive ind^", "^string_of_int i^")"
-
-
-(* /spiwack *)
-- 
cgit v1.2.3