Ring: replaced various generic = on constr by eq_constr, destructors etc.

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

1 files changed, 25 insertions, 19 deletions

diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 6dd2a0c6e..9a252dfb7 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -135,7 +135,7 @@ let mkLApp(fc,v) = mkApp(Lazy.force fc, v)
 module OperSet =
   Set.Make (struct
 	      type t = global_reference
-	      let compare = (Pervasives.compare : t->t->int)
+	      let compare = (RefOrdered.compare : t->t->int)
 	    end)
 
 type morph =
@@ -377,8 +377,14 @@ Builds
 
 *)
 
+module Constrhash = Hashtbl.Make
+  (struct type t = constr
+	  let equal = eq_constr
+	  let hash = hash_constr
+   end)
+
 let build_spolynom gl th lc =
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
   (* aux creates the spolynom p by a recursive destructuration of c
@@ -392,14 +398,14 @@ let build_spolynom gl th lc =
       | _ when closed_under th.th_closed c ->
 	  mkLApp(coq_SPconst, [|th.th_a; c |])
       | _ ->
-	  try Hashtbl.find varhash c
+	  try Constrhash.find varhash c
 	  with Not_found ->
 	    let newvar =
               mkLApp(coq_SPvar, [|th.th_a; (path_of_int !counter) |]) in
 	    begin
 	      incr counter;
 	      varlist := c :: !varlist;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in
@@ -434,7 +440,7 @@ Builds
 *)
 
 let build_polynom gl th lc =
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c =
@@ -455,14 +461,14 @@ let build_polynom gl th lc =
       | _ when closed_under th.th_closed c ->
 	  mkLApp(coq_Pconst, [|th.th_a; c |])
       | _ ->
-	  try Hashtbl.find varhash c
+	  try Constrhash.find varhash c
 	  with Not_found ->
 	    let newvar =
               mkLApp(coq_Pvar, [|th.th_a; (path_of_int !counter) |]) in
 	    begin
 	      incr counter;
 	      varlist := c :: !varlist;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in
@@ -498,7 +504,7 @@ Builds
 *)
 
 let build_aspolynom gl th lc =
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
   (* aux creates the aspolynom p by a recursive destructuration of c
@@ -512,13 +518,13 @@ let build_aspolynom gl th lc =
       | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0
       | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1
       | _ ->
-	  try Hashtbl.find varhash c
+	  try Constrhash.find varhash c
 	  with Not_found ->
 	    let newvar = mkLApp(coq_ASPvar, [|(path_of_int !counter) |]) in
 	    begin
 	      incr counter;
 	      varlist := c :: !varlist;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in
@@ -552,7 +558,7 @@ Builds
 *)
 
 let build_apolynom gl th lc =
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c =
@@ -572,14 +578,14 @@ let build_apolynom gl th lc =
       | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0
       | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_AP1
       | _ ->
-	  try Hashtbl.find varhash c
+	  try Constrhash.find varhash c
 	  with Not_found ->
 	    let newvar =
               mkLApp(coq_APvar, [| path_of_int !counter |]) in
 	    begin
 	      incr counter;
 	      varlist := c :: !varlist;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in
@@ -613,7 +619,7 @@ Builds
 *)
 
 let build_setpolynom gl th lc =
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c =
@@ -634,14 +640,14 @@ let build_setpolynom gl th lc =
       | _ when closed_under th.th_closed c ->
 	  mkLApp(coq_SetPconst, [| th.th_a; c |])
       | _ ->
-	  try Hashtbl.find varhash c
+	  try Constrhash.find varhash c
 	  with Not_found ->
 	    let newvar =
               mkLApp(coq_SetPvar, [| th.th_a; path_of_int !counter |]) in
 	    begin
 	      incr counter;
 	      varlist := c :: !varlist;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in
@@ -680,7 +686,7 @@ Builds
 *)
 
 let build_setspolynom gl th lc =
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c =
@@ -692,14 +698,14 @@ let build_setspolynom gl th lc =
       | _ when closed_under th.th_closed c ->
 	  mkLApp(coq_SetSPconst, [| th.th_a; c |])
       | _ ->
-	  try Hashtbl.find varhash c
+	  try Constrhash.find varhash c
 	  with Not_found ->
 	    let newvar =
               mkLApp(coq_SetSPvar, [|th.th_a; path_of_int !counter |]) in
 	    begin
 	      incr counter;
 	      varlist := c :: !varlist;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in