From d0eb3e2cd98bbeb08db3aa32d233233569d50351 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 28 Feb 2014 15:18:45 +0100 Subject: Removing Pervasives.compare in Termdn. --- tactics/btermdn.ml | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) (limited to 'tactics/btermdn.ml') 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) -- cgit v1.2.3