diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2303.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2303.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2303.v b/test-suite/bugs/closed/shouldsucceed/2303.v deleted file mode 100644 index e614b9b5..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2303.v +++ /dev/null @@ -1,4 +0,0 @@ -Class A := a: unit. -Class B (x: unit). -Axiom H: forall x: A, @B x -> x = x -> unit. -Definition Field (z: A) (m: @B z) x := (@H _ _ x) = z. |