diff options
| author |  xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-14 09:58:28 +0000 |
|---|---|---|
| committer | xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-14 09:58:28 +0000 |
| commit | 4a4b11e9932dc824e7dd88ef6db971f1a1dab1a3 (patch) | |
| tree | 5ffcd8ec7b78269c12e6ed039d0b8d7e0dfa114e /plugins/rtauto | |
| parent | 5407fbfe5c091e4d97d7a7fbe04941b860510f8e (diff) | |
Avoid polymorphic comparison (plugins/rtauto).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16886 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/proof_search.ml | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 9aad65f29..101fe288b 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -62,7 +62,30 @@ type form= | Conjunct of form * form | Disjunct of form * form -module FOrd = struct type t = form let compare = Pervasives.compare (** FIXME *) end +module FOrd = struct + type t = form + let rec compare x y = + match x, y with + | Bot, Bot -> 0 + | Bot, _ -> -1 + | Atom _, Bot -> 1 + | Atom a1, Atom a2 -> Pervasives.compare a1 a2 + | Atom _, _ -> -1 + | Arrow _, (Bot | Atom _) -> 1 + | Arrow (f1, g1), Arrow (f2, g2) -> + let cmp = compare f1 f2 in + if cmp = 0 then compare g1 g2 else cmp + | Arrow _, _ -> -1 + | Conjunct _, (Bot | Atom _ | Arrow _) -> 1 + | Conjunct (f1, g1), Conjunct (f2, g2) -> + let cmp = compare f1 f2 in + if cmp = 0 then compare g1 g2 else cmp + | Conjunct _, _ -> -1 + | Disjunct _, (Bot | Atom _ | Arrow _ | Conjunct _) -> 1 + | Disjunct (f1, g1), Disjunct (f2, g2) -> + let cmp = compare f1 f2 in + if cmp = 0 then compare g1 g2 else cmp +end module Fmap = Map.Make(FOrd) type sequent = |