From 4a4b11e9932dc824e7dd88ef6db971f1a1dab1a3 Mon Sep 17 00:00:00 2001
From: xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 14 Oct 2013 09:58:28 +0000
Subject: Avoid polymorphic comparison (plugins/rtauto).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16886 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/rtauto/proof_search.ml | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

(limited to 'plugins/rtauto')

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 =
-- 
cgit v1.2.3