diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-28 15:18:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-28 21:52:16 +0100 |
| commit | d0eb3e2cd98bbeb08db3aa32d233233569d50351 (patch) | |
| tree | a93f71a39e922799a1755fc33b13c27fe0684551 /tactics/btermdn.ml | |
| parent | dc438047cc7d20d4f2df6ab703689814a7552623 (diff) | |
Removing Pervasives.compare in Termdn.
Diffstat (limited to 'tactics/btermdn.ml')
| -rw-r--r-- | tactics/btermdn.ml | 19 |
1 files changed, 5 insertions, 14 deletions
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) |