diff options
| author | aspiwack | 2007-12-18 12:19:12 +0000 |
|---|---|---|
| committer | aspiwack | 2007-12-18 12:19:12 +0000 |
| commit | f3eaf2869e84c942d56a7fe0cc459d9943e4b059 (patch) | |
| tree | 4a67e700f35e74324cece25f50325758e43dcb03 /kernel/names.mli | |
| parent | 0e1b31da1546b7ac0dd3664e73ba05127320bed9 (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.mli')
| -rw-r--r-- | kernel/names.mli | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index dee798da09..64edf1702e 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -174,15 +174,3 @@ type inv_rel_key = int (* index in the [rel_context] part of environment of de Bruijn indice *) type id_key = inv_rel_key tableKey - - - -(* spiwack : function used for printing identifiers *) -val string_of_identifier : identifier-> string -val string_of_module_ident : module_ident-> string -val string_of_dir_path : dir_path -> string -val string_of_name : name -> string -val string_of_constant : constant -> string -val string_of_mutual_inductive : mutual_inductive -> string -val string_of_inductive : inductive -> string -val string_of_constructor : constructor -> string |