- 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

2 files changed, 38 insertions, 22 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
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 88b4e650f1..2b512d76f1 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1679,22 +1679,23 @@ struct
     
   let hash = HInstancestruct.hash
     
-  let share a =
-    let len = Array.length a in
-      if Int.equal len 0 then (empty, 0)
-      else begin
-	let accu = ref 0 in
-	  for i = 0 to len - 1 do
-	    let l = Array.unsafe_get a i in
-	    let l', h = Level.hcons l, Level.hash l in
-	      accu := Hashset.Combine.combine !accu h;
-	      if l' == l then () 
-	      else Array.unsafe_set a i l'
-	  done;
-	  (* [h] must be positive. *)
-	  let h = !accu land 0x3FFFFFFF in
-	    (a, h)
-      end
+  let share a = (a, hash a)
+
+    (* let len = Array.length a in *)
+    (*   if Int.equal len 0 then (empty, 0) *)
+    (*   else begin *)
+    (* 	let accu = ref 0 in *)
+    (* 	  for i = 0 to len - 1 do *)
+    (* 	    let l = Array.unsafe_get a i in *)
+    (* 	    let l', h = Level.hcons l, Level.hash l in *)
+    (* 	      accu := Hashset.Combine.combine !accu h; *)
+    (* 	      if l' == l then ()  *)
+    (* 	      else Array.unsafe_set a i l' *)
+    (* 	  done; *)
+    (* 	  (\* [h] must be positive. *\) *)
+    (* 	  let h = !accu land 0x3FFFFFFF in *)
+    (* 	    (a, h) *)
+    (*   end *)
 	      
   let empty = hcons [||]