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

2 files changed, 29 insertions, 2 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index a04631580e..2363789fab 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)
diff --git a/lib/pp.ml b/lib/pp.ml
index 331408b6d6..c0b23fd870 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -20,6 +20,7 @@ module Glue : sig
   val atom : 'a -> 'a t
   val glue : 'a t -> 'a t -> 'a t
   val empty : 'a t
+  val is_empty : 'a t -> bool
   val iter : ('a -> unit) -> 'a t -> unit
 
 end = struct
@@ -29,6 +30,7 @@ end = struct
   let atom x = [x]
   let glue x y = y @ x
   let empty = []
+  let is_empty x = x = []
 
   let iter f g = List.iter f (List.rev g)
 
@@ -105,7 +107,7 @@ let (++) = Glue.glue
 
 let app = Glue.glue
 
-let is_empty g = g = Glue.empty
+let is_empty g = Glue.is_empty g
 
 
 (* Compute length of an UTF-8 encoded string