diff options
| -rw-r--r-- | interp/constrextern.ml | 5 | ||||
| -rw-r--r-- | interp/notation.ml | 23 | ||||
| -rw-r--r-- | interp/notation.mli | 2 | ||||
| -rw-r--r-- | lib/util.ml | 6 | ||||
| -rw-r--r-- | lib/util.mli | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 17 |
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. |