- Fix index-list to show computational relations for rewriting files.

- Fix hasheq which didn't have a case for Proj making hashconsing exponentially slower.

Conflicts:
	kernel/constr.ml
	kernel/univ.ml
	proofs/proof_global.ml

1 files changed, 21 insertions, 6 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index ac2c4418e4..271691e029 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -723,8 +723,8 @@ let hasheq t1 t2 =
     | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 && t1 == t2 && c1 == c2
     | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) ->
       n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2
-    | Proj (c1,t1), Proj (c2,t2) -> c1 == c2 && t1 == t2
     | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2
+    | Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2
     | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2
     | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2
     | Ind ((sp1,i1),u1), Ind ((sp2,i2),u2) -> 
@@ -807,8 +807,8 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
 	(Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
       | Proj (p,c) ->
         let c, hc = sh_rec c in
-        let p' = sh_con p in
-          (Proj (p', c), combinesmall 17 (Hashtbl.hash p'))
+	let p' = sh_con p in
+	  (Proj (p', c), combinesmall 17 (combine (Constant.hash p') hc))
       | Const (c,u) ->
 	let c' = sh_con c in
 	let u', hu = sh_instance u in
@@ -973,9 +973,24 @@ module Hsorts =
 let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ
 let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
 
-let hcons_pconstruct (c,u) = (hcons_construct c, Univ.Instance.hcons u)
-let hcons_pind (i,u) = (hcons_ind i, Univ.Instance.hcons u)
-let hcons_pcon (c,u) = (hcons_con c, Univ.Instance.hcons u)
+let hcons_pconstruct (c,u as x) = 
+  let c' = hcons_construct c in 
+    if c' == c then x
+    else (c', u)
+
+let hcons_pind (i,u as x) = 
+  let i' = hcons_ind i in 
+    if i' == i then x 
+    else i', u
+
+let hcons_pcon (c,u as x) =
+  let c' = hcons_con c in
+    if c' == c then x
+    else c', u
+
+(* let hcons_pconstruct (c,u) = (hcons_construct c, Univ.Instance.hcons u) *)
+(* let hcons_pind (i,u) = (hcons_ind i, Univ.Instance.hcons u) *)
+(* let hcons_pcon (c,u) = (hcons_con c, Univ.Instance.hcons u) *)
 
 let hcons =
   hashcons