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

1 files changed, 0 insertions, 35 deletions

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 8103bdafb..c746e4199 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -52,42 +52,7 @@ let type_constructor mind mib typ params =
     let _,ctyp = decompose_prod_n nparams ctyp in   
     substl (List.rev (Array.to_list params)) ctyp
 
-(* arnaud: to clean 
-(* spiwack: auxiliary fonction for decompiling 31-bit integers
-   into their corresponding constr *)
-let constr_of_int31 =
-  let nth_digit_plus_one i n = (* calculates the nth (starting with 0)
-                                  digit of i and adds 1 to it 
-                                  (nth_digit_plus_one 1 3 = 2) *)
-      if (land) i ((lsl) 1 n) = 0 then
-         1
-      else
-         2
-  in
-  fun tag -> fun ind->
-  let digit_ind = Retroknowledge.digits_of_int31 ind 
-  in
-  let array_of_int i =
-    Array.init 31 (fun n -> mkConstruct(digit_ind, nth_digit_plus_one i (30-n)))
-  in
-    mkApp(mkConstruct(ind, 1), array_of_int tag) *)
 
-(* /spiwack *)
-(* arnaud
-let construct_of_constr_const env tag typ =
-  let ind,params = find_rectype env typ in
-  (* arnaud:improve comment ? *)
-  (* spiwack: branching for 31-bits integers *)
-(* arnaud:
-  if Retroknowledge.isInt31t ind then
-    constr_of_int31 tag ind
-  else *)
-  try 
-    retroknowledge Retroknowledge.get_vm_decompile_constant_info env (Ind ind) tag
-  with Not_found ->
-    let (_,mip) = lookup_mind_specif env ind in
-    let i = invert_tag true tag mip.mind_reloc_tbl in
-    applistc (mkConstruct(ind,i))  params *)
 
 let construct_of_constr const env tag typ =
   let (mind,_ as ind), allargs = find_rectype_a env typ in