Some more hand-written comparison functions to avoid polymorphic comparison.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16887 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 26 insertions, 1 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index a04631580..2363789fa 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -207,6 +207,18 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of kernel_name
 
+let compare_interp_rule x y =
+  match x, y with
+  | NotationRule (sno1, n1), NotationRule (sno2, n2) ->
+      (match sno1, sno2 with
+      | None, None -> String.compare n1 n2
+      | None, Some _ -> -1
+      | Some sn1, Some sn2 -> String.compare sn1 sn2
+      | Some _, None -> 1)
+  | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2
+  | NotationRule _, SynDefRule _ -> -1
+  | SynDefRule _, NotationRule _ -> 1
+
 (* We define keys for glob_constr and aconstr to split the syntax entries
    according to the key of the pattern (adapted from Chet Murthy by HH) *)
 
@@ -226,7 +238,20 @@ module KeyMap = Map.Make(KeyOrd)
 module InterpretationOrd =
 struct
   type t = interp_rule * interpretation * int option
-  let compare = Pervasives.compare (* FIXME: to be explicitely written *)
+  let compare (ir1, i1, io1) (ir2, i2, io2) =
+    let cmp = compare_interp_rule ir1 ir2 in
+    if cmp = 0 then
+      let cmp' = Pervasives.compare i1 i2 in (* FIXME: to be explicitely written *)
+      if cmp' = 0 then
+        match io1, io2 with
+        | None, None -> 0
+        | None, Some _ -> -1
+        | Some x, Some y -> Pervasives.compare x y
+        | Some _, None -> 1
+      else
+        cmp'
+    else
+      cmp
 end
 
 module InterpretationSet = Set.Make (InterpretationOrd)