diff options
| author | regisgia | 2013-01-06 18:57:33 +0000 |
|---|---|---|
| committer | regisgia | 2013-01-06 18:57:33 +0000 |
| commit | 890dc4c4260e7782c8550a631163796a40e06d99 (patch) | |
| tree | 87e6c76d2d536b9250af1408a2c49fdfa07e2d07 /kernel | |
| parent | 3ac6551b239281f2bd985488ad3eb36b9b107115 (diff) | |
* Kernel/Terms:
Fix an inconsistency in the hashing function of [constr]s.
(Thanks to Thomas Braibant for having pointed this out.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16116 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 9cb38e33da..a66e5fb2be 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1315,15 +1315,15 @@ let hcons_term (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Const c -> (Const (sh_con c), combinesmall 9 (Hashtbl.hash c)) | Ind ((kn,i) as ind) -> - (Ind (sh_ind ind), combinesmall 9 (combine (Hashtbl.hash kn) i)) + (Ind (sh_ind ind), combinesmall 10 (combine (Hashtbl.hash kn) i)) | Construct (((kn,i),j) as c)-> - (Construct (sh_construct c), combinesmall 10 (combine3 (Hashtbl.hash kn) i j)) + (Construct (sh_construct c), combinesmall 11 (combine3 (Hashtbl.hash kn) i j)) | Case (ci,p,c,bl) -> let p, hp = sh_rec p and c, hc = sh_rec c in let hbl = hash_term_array bl in let hbl = combine (combine hc hp) hbl in - (Case (sh_ci ci, p, c, bl), combinesmall 11 hbl) + (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl) | Fix (ln,(lna,tl,bl)) -> let hbl = hash_term_array bl in let htl = hash_term_array tl in @@ -1374,11 +1374,11 @@ let rec hash_constr t = | Const c -> combinesmall 9 (Hashtbl.hash c) (* TODO: proper hash function for constants *) | Ind (kn,i) -> - combinesmall 9 (combine (Hashtbl.hash kn) i) + combinesmall 10 (combine (Hashtbl.hash kn) i) | Construct ((kn,i),j) -> - combinesmall 10 (combine3 (Hashtbl.hash kn) i j) + combinesmall 11 (combine3 (Hashtbl.hash kn) i j) | Case (_ , p, c, bl) -> - combinesmall 11 (combine3 (hash_constr c) (hash_constr p) (hash_term_array bl)) + combinesmall 12 (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)) -> |