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

10 files changed, 5 insertions, 137 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 84d04d67e5..ceba6e82a0 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -235,7 +235,3 @@ type block =
  
 let draw_instr c =
   fprintf std_formatter "@[<v 0>%a@]" instruction_list c
-
-let string_of_instr c =
-  fprintf str_formatter "@[<v 0>%a@]" instruction_list c;
-  flush_str_formatter ()
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 86b465543e..c24b5a5301 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -132,8 +132,6 @@ type comp_env = {
 
 val draw_instr : bytecodes -> unit
 
-val string_of_instr : bytecodes -> string
-
 
 
 (*spiwack: moved this here because I needed it for retroknowledge *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 2664abe1fc..721134252b 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -335,7 +335,7 @@ let rec str_const c =
   | App(f,args) -> 
       begin
 	match kind_of_term f with
-	| Construct(((kn,j),i) as cstr) -> 
+	| Construct((kn,j),i) -> (* arnaud: Construct(((kn,j),i) as cstr) -> *)
             begin
 	    let oib = lookup_mind kn !global_env in
 	    let oip = oib.mind_packets.(j) in
@@ -405,7 +405,7 @@ let rec str_const c =
 	| _ -> Bconstr c
       end
   | Ind ind -> Bstrconst (Const_ind ind)
-  | Construct ((kn,j),i as cstr) ->  
+  | Construct ((kn,j),i) ->  (*arnaud: Construct ((kn,j),i as cstr) ->  *)
       begin
       (* spiwack: tries first to apply the run-time compilation 
            behavior of the constructor, as in 2/ above *)
@@ -664,7 +664,7 @@ and compile_str_cst reloc sc sz cont =
 (* spiwack : compilation of constants with their arguments. 
    Makes a special treatment with 31-bit integer addition *)
 and compile_const =
-  let code_construct kn cont = 
+(*arnaud:  let code_construct kn cont = 
      let f_cont = 
          let else_lbl = Label.create () in
          Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
@@ -672,11 +672,11 @@ and compile_const =
          (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
           Kgetglobal (get_allias !global_env kn)::
           Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
-     in
+     in 
      let lbl = Label.create () in 
      fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)];
      Kclosure(lbl, 0)::cont
-  in
+  in *)
   fun reloc-> fun  kn -> fun args -> fun sz -> fun cont ->
   let nargs = Array.length args in
   (* spiwack: checks if there is a specific way to compile the constant
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 829ac46e26..dfdcb07473 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -14,7 +14,6 @@ val compile_constant_body :
                                  (* opaque *) (* boxed *)
 
 
-(* arnaud : a commenter *)
 (* spiwack: this function contains the information needed to perform
             the static compilation of int31 (trying and obtaining
             a 31-bit integer in processor representation at compile time) *)
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 *)
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
diff --git a/kernel/term.ml b/kernel/term.ml
index b09bd4aea7..ad4bd2bda2 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1177,52 +1177,3 @@ let (hcons1_constr, hcons1_types) = hcons_constr (hcons_names())
 (*******)
 (* Type of abstract machine values *)
 type values
-
-
-
-(* spiwack : internal representation printing *)
-let string_of_sorts =
-  function 
-  | Prop Pos -> "Prop Pos"
-  | Prop Null -> "Prop Null"
-  | Type u -> "Type "^string_of_universe u
-
-let string_of_cast_kind = 
-  function
-  |VMcast -> "VMcast"
-  | DEFAULTcast -> "DEFAULTcast"
-
-let rec string_of_constr = 
-  let string_of_term string_of_expr string_of_type = function
-  | Rel i -> "Rel "^string_of_int i
-  | Var id -> "Var "^string_of_identifier id
-  | Meta mv -> "Meta "^"mv?" (* need a function for printing metavariables *)
-  | Evar ev -> "Evar "^"ev?" (* ??     of 'constr pexistential *)
-  | Sort s -> "Sort "^string_of_sorts s
-  | Cast (e,ck,t) -> 
-         "Cast ("^string_of_expr e^", "^string_of_cast_kind ck^", "^
-                 string_of_type t^")" 
-  | Prod (n, t1, t2) -> 
-          "Prod ("^string_of_name n^", "^string_of_type t1^", "^
-                   string_of_type t2^")"  
-  | Lambda (n,t,e) ->
-          "Lambda ("^string_of_name n^", "^string_of_type t^", "^
-                    string_of_expr e^")"
-  | LetIn (n, e1, t, e2) -> 
-           "LetIn ("^string_of_name n^", "^string_of_expr e1^", "^
-           string_of_type t^", "^string_of_expr e2^")"
-  | App   (e, args) ->  "App ("^string_of_expr e^", [|"^
-          String.concat "; " (Array.to_list (Array.map string_of_expr args)) ^
-          "|])"
-  | Const c ->  "Const "^string_of_constant c
-  | Ind   ind ->  "Ind "^string_of_inductive ind
-  | Construct ctr -> "Construct "^string_of_constructor ctr
-  | Case(_,_,_,_)  -> "Case ..."    
-             (*    of case_info * 'constr * 'constr * 'constr array   *)
-  | Fix _  -> "Fix ..."  (*    of ('constr, 'types) pfixpoint *)
-  | CoFix _ -> "CoFix ..."  (*     of ('constr, 'types) pcofixpoint *)
-in 
-fun x -> string_of_term string_of_constr string_of_constr x
-
-
-(* /spiwack *)
diff --git a/kernel/term.mli b/kernel/term.mli
index b0387417cc..b5304b6511 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -543,9 +543,3 @@ val hcons1_types : types -> types
 (**************************************)
 
 type values
-
-
-(*************************************************************)
-
-(* spiwack: printing of internal representation of constr *)
-val string_of_constr : constr -> string
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7a7e0bb5a0..a127fd5c09 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -578,17 +578,3 @@ let hcons1_univ u =
   let _,_,hdir,_,_,_ = Names.hcons_names() in
   Hashcons.simple_hcons Huniv.f hdir u
 
-
-
-(* spiwack: function for internal representation printing *)
-let string_of_universe =
-  let string_of_universe_level = function
-  | Base -> "Base"
-  | Level (path,i) -> "Level ("^Names.string_of_dir_path path^", "^string_of_int i^")"
-in
-function 
-  | Atom u -> "Atom "^string_of_universe_level u
-  | Max (l1,l2) -> "Max (["^
-               String.concat "; " (List.map string_of_universe_level l1)^"], ["^
-               String.concat "; " (List.map string_of_universe_level l2)
-               ^"])"
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 6c709bc83d..52af808e3c 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -79,7 +79,3 @@ val pr_universes : universes -> Pp.std_ppcmds
 val dump_universes : out_channel -> universes -> unit
 
 val hcons1_univ : universe -> universe
-
-
-(* spiwack: function for internal representation printing *)
-val string_of_universe : universe -> string