* Kernel/Term

  Remove an unsound optimization.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13661 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 4 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index cca5c4c9b..830cabd96 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -174,7 +174,7 @@ let array_eqeq t1 t2 =
   Array.length t1 = Array.length t2 && 
   let rec aux i = 
     (i = Array.length t1) || (t1.(i) == t2.(i) && aux (i + 1))
-  in aux 0
+  in aux 0 
 
 let comp_term t1 t2 =
   match t1, t2 with
@@ -297,16 +297,15 @@ let combinesmall x y = beta * x + y
    representation for [constr] using [hash_consing_functions] on
    leaves. *)
 let hcons_term (sh_sort,sh_con,sh_kn,sh_na,sh_id) =
-  let accu = ref 0 in 
 
   let rec hash_term_array t = 
-    accu := 0;
+    let accu = ref 0 in 
     for i = 0 to Array.length t - 1 do 
       let x, h = sh_rec t.(i) in 
       accu := combine !accu h; 
       t.(i) <- x
     done;
-    (t, !accu)
+    (t, !accu) 
 
   and hash_term t =
     match t with