Removing Pervasives.compare in Termdn.

3 files changed, 17 insertions, 41 deletions

diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index dd1309290..d22e032df 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -93,13 +93,7 @@ struct
   let compare cmp t1 t2 = match t1, t2 with
   | DRel, DRel -> 0
   | DSort, DSort -> 0
-  | DRef gr1, DRef gr2 ->
-    begin match gr1, gr2 with
-    | ConstRef c1, ConstRef c2 -> Constant.CanOrd.compare c1 c2
-    | IndRef i1, IndRef i2 -> ind_ord i1 i2
-    | ConstructRef c1, ConstructRef c2 -> constructor_ord c1 c2
-    | _ -> Pervasives.compare gr1 gr2 (** OK **)
-    end
+  | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2
   | DCtx (tl1, tr1), DCtx (tl2, tr2)
   | DLambda (tl1, tr1), DCtx (tl2, tr2)
   | DApp (tl1, tr1), DCtx (tl2, tr2) ->
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 0a1845322..76119a2ec 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 432a4123b..b5a7359d6 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