diff options
| author | Vincent Laporte | 2019-04-24 11:37:42 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-29 09:51:05 +0000 |
| commit | 2c18da20b260c55d8da49b1bb4f53e72dbc75a87 (patch) | |
| tree | 0621fa3e706a676053c076f90c73f8e042226e6d /test-suite | |
| parent | 4e25d51b89b66d4b9c982e85a5de9645e7e537ad (diff) | |
Revert #9249
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 17 |
2 files changed, 0 insertions, 19 deletions
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. |