aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
diff options
context:
space:
mode:
authoraspiwack2007-12-18 12:19:12 +0000
committeraspiwack2007-12-18 12:19:12 +0000
commitf3eaf2869e84c942d56a7fe0cc459d9943e4b059 (patch)
tree4a67e700f35e74324cece25f50325758e43dcb03 /kernel/names.ml
parent0e1b31da1546b7ac0dd3664e73ba05127320bed9 (diff)
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
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml40
1 files changed, 0 insertions, 40 deletions
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 *)