Removing Pervasives.compare in Termdn.

2 files changed, 16 insertions, 34 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 0a18453229..76119a2ec4 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -26,23 +26,14 @@ struct
 
   module X = struct
     type t = constr_pattern*int
-    let compare = Pervasives.compare 
+    let compare = Pervasives.compare (** FIXME *)
   end
 
  module Y = struct 
-     type t = Term_dn.term_label
-     let compare x y = 
-       let make_name n =
-	 match n with
-	 | Term_dn.GRLabel(ConstRef con) -> 
-	     Term_dn.GRLabel(ConstRef(constant_of_kn(canonical_con con)))
-	 | Term_dn.GRLabel(IndRef (kn,i)) ->
-	     Term_dn.GRLabel(IndRef(mind_of_kn(canonical_mind kn),i))
-	 | Term_dn.GRLabel(ConstructRef ((kn,i),j ))->
-	     Term_dn.GRLabel(ConstructRef((mind_of_kn(canonical_mind kn),i),j))
-	 | k -> k
-       in
-	 Pervasives.compare (make_name x) (make_name y)
+    type t = Term_dn.term_label
+    let compare t1 t2 = match t1, t2 with
+    | Term_dn.GRLabel gr1, Term_dn.GRLabel gr2 -> RefOrdered.compare gr1 gr2
+    | _ -> Pervasives.compare t1 t2 (** OK *)
  end
  
  module Dn = Dn.Make(X)(Y)(Z)
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 432a4123b6..b5a7359d6b 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -25,31 +25,22 @@ struct
     let compare = Pervasives.compare (** FIXME *)
   end
 
-  type term_label = 
+  type term_label =
     | GRLabel of global_reference
-    | ProdLabel 
+    | ProdLabel
     | LambdaLabel
     | SortLabel
-	
-  module Y =  struct 
-     type t = term_label
-        let compare x y = 
-       let make_name n =
-	 match n with
-	 | GRLabel(ConstRef con) -> 
-	     GRLabel(ConstRef(constant_of_kn(canonical_con con)))
-	 | GRLabel(IndRef (kn,i)) ->
-	     GRLabel(IndRef(mind_of_kn(canonical_mind kn),i))
-	 | GRLabel(ConstructRef ((kn,i),j ))->
-	     GRLabel(ConstructRef((mind_of_kn(canonical_mind kn),i),j))
-	 | k -> k
-       in
-	 Pervasives.compare (make_name x) (make_name y)
+
+  module Y =  struct
+    type t = term_label
+    let compare t1 t2 = match t1, t2 with
+    | GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2
+    | _ -> Pervasives.compare t1 t2 (** OK *)
   end
-       
-      
+
+
   module Dn = Dn.Make(X)(Y)(Z)
-      
+
   type t = Dn.t
 
   type 'a lookup_res = 'a Dn.lookup_res