Revert #9249

7 files changed, 5 insertions, 54 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 488c9a740f..717c476526 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -67,7 +67,10 @@ let print_no_symbol = ref false
 
 (**********************************************************************)
 (* Turning notations and scopes on and off for printing *)
-module IRuleSet = InterpRuleSet
+module IRuleSet = Set.Make(struct
+    type t = interp_rule
+    let compare x y = Pervasives.compare x y
+  end)
 
 let inactive_notations_table =
   Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty)
diff --git a/interp/notation.ml b/interp/notation.ml
index 56504db04e..9e338e7df9 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -50,25 +50,15 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with
 | InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2
 | (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false
 
-let notation_entry_level_compare s1 s2 = match (s1,s2) with
-| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> 0
-| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) ->
-   pair_compare String.compare Int.compare (s1,n1) (s2,n2)
-| InConstrEntrySomeLevel, _ -> -1
-| InCustomEntryLevel _, _ -> 1
-
 let notation_eq (from1,ntn1) (from2,ntn2) =
   notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
 
 let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s
 
-let notation_compare =
-  pair_compare notation_entry_level_compare String.compare
-
 module NotationOrd =
   struct
     type t = notation
-    let compare = notation_compare
+    let compare = Pervasives.compare
   end
 
 module NotationSet = Set.Make(NotationOrd)
@@ -188,17 +178,6 @@ type scoped_notation_rule_core = scope_name * notation * interpretation * int op
 type notation_rule_core = interp_rule * interpretation * int option
 type notation_rule = notation_rule_core * delimiters option * bool
 
-let interp_rule_compare r1 r2 = match r1, r2 with
-  | NotationRule (sc1,ntn1), NotationRule (sc2,ntn2) ->
-      pair_compare (Option.compare String.compare) notation_compare (sc1,ntn1) (sc2,ntn2)
-  | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2
-  | (NotationRule _ | SynDefRule _), _ -> -1
-
-module InterpRuleSet = Set.Make(struct
-    type t = interp_rule
-    let compare = interp_rule_compare
-  end)
-
 (* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and  *)
 
 type uninterp_scope_elem =
diff --git a/interp/notation.mli b/interp/notation.mli
index 57e2be16b9..017023c133 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -216,8 +216,6 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of KerName.t
 
-module InterpRuleSet : Set.S with type elt = interp_rule
-
 val declare_notation_interpretation : notation -> scope_name option ->
       interpretation -> notation_location -> onlyprint:bool -> unit
 
diff --git a/lib/util.ml b/lib/util.ml
index 0389336258..38d73d3453 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -20,12 +20,6 @@ let on_pi1 f (a,b,c) = (f a,b,c)
 let on_pi2 f (a,b,c) = (a,f b,c)
 let on_pi3 f (a,b,c) = (a,b,f c)
 
-(* Comparing pairs *)
-
-let pair_compare cmpx cmpy (x1,y1 as p1) (x2,y2 as p2) =
-  if p1 == p2 then 0 else
-  let c = cmpx x1 x2 in if c == 0 then cmpy y1 y2 else c
-
 (* Projections from triplets *)
 
 let pi1 (a,_,_) = a
diff --git a/lib/util.mli b/lib/util.mli
index fa3b622621..1eb60f509a 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -17,10 +17,6 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
 val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
 val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b
 
-(** Comparing pairs *)
-
-val pair_compare : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a * 'b -> 'a * 'b -> int)
-
 (** Mapping under triple *)
 
 val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 5bf4ec7bfb..ca20575f1a 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -49,8 +49,6 @@ myAnd1 True True
      : Prop
 r 2 3
      : Prop
-Notation Cn := Foo.FooCn
-Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn
 let v := 0%test17 in v : myint63
      : myint63
 fun y : nat => # (x, z) |-> y & y
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index b33ad17ed4..3311549013 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -181,23 +181,6 @@ Check r 2 3.
 
 End I.
 
-(* Fixing a bug reported by G. Gonthier in #9207 *)
-
-Module J.
-
-Module Import Mfoo.
-Module Foo.
-Definition FooCn := 2.
-Module Bar.
-Notation Cn := FooCn.
-End Bar.
-End Foo.
-Export Foo.Bar.
-End Mfoo.
-About Cn.
-
-End J.
-
 Require Import Coq.Numbers.Cyclic.Int63.Int63.
 Module NumeralNotations.
   Module Test17.