Term: fix hash_constr to hash modulo casts & names (like compare_constr)

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

1 files changed, 13 insertions, 17 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 83c417d95..9ff8ee9ca 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1338,34 +1338,30 @@ let rec hash_constr t =
   match kind_of_term t with
     | Var i -> combinesmall 1 (Hashtbl.hash i)
     | Sort s -> combinesmall 2 (Hashtbl.hash s)
-    | Cast (c, k, t) ->
-      combinesmall 3 (combine3 (hash_constr c) (Hashtbl.hash k) (hash_constr t))
-    | Prod (na,t,c) ->
-      combinesmall 4 (combine3 (Hashtbl.hash na) (hash_constr t) (hash_constr c))
-    | Lambda (na,t,c) ->
-      combinesmall 5 (combine3 (Hashtbl.hash na) (hash_constr t) (hash_constr c))
-    | LetIn (na,b,t,c) ->
-      combinesmall 6 (combine4 (Hashtbl.hash na) (hash_constr b) (hash_constr t) (hash_constr c))
+    | Cast (c, _, _) -> hash_constr c
+    | Prod (_, t, c) -> combinesmall 4 (combine (hash_constr t) (hash_constr c))
+    | Lambda (_, t, c) -> combinesmall 5 (combine (hash_constr t) (hash_constr c))
+    | LetIn (_, b, t, c) ->
+      combinesmall 6 (combine3 (hash_constr b) (hash_constr t) (hash_constr c))
     | App (c,l) ->
       combinesmall 7 (combine (hash_term_array l) (hash_constr c))
     | Evar (e,l) ->
       combinesmall 8 (combine (Hashtbl.hash e) (hash_term_array l))
     | Const c ->
-      combinesmall 9 (Hashtbl.hash c)
+      combinesmall 9 (Hashtbl.hash c)	(* TODO: proper hash function for constants *)
     | Ind (kn,i) ->
       combinesmall 9 (combine (Hashtbl.hash kn) i)
     | Construct ((kn,i),j) ->
       combinesmall 10 (combine3 (Hashtbl.hash kn) i j)
-    | Case (ci,p,c,bl) -> (* TO DO: extract ind_kn *)
-      combinesmall 11 (combine (combine (hash_constr c) (hash_constr p)) (hash_term_array bl))
-    | Fix (ln,(lna,tl,bl)) ->
-      let h = combine (hash_term_array bl) (hash_term_array tl) in
-      combinesmall 13 (combine (Hashtbl.hash lna) h)
-    | CoFix(ln,(lna,tl,bl)) ->
-      let h = combine (hash_term_array bl) (hash_term_array tl) in
-       combinesmall 14 (combine (Hashtbl.hash lna) h)
+    | Case (_ , p, c, bl) ->
+      combinesmall 11 (combine3 (hash_constr c) (hash_constr p) (hash_term_array bl))
+    | Fix (ln ,(_, tl, bl)) ->
+      combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl))
+    | CoFix(ln, (_, tl, bl)) ->
+       combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl))
     | Meta n -> combinesmall 15 n
     | Rel n -> combinesmall 16 n
+
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine (hash_constr t) acc) 0 t