blob: 78ed3744325d3d95572c0955723b79fe4e42e9d1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
From Coq Require Import ssreflect.
From Coq Require Import ssrbool.
Set Printing All.
Set Debug Ssreflect.
Class Class := { sort : Type ; op : sort -> bool }.
Coercion sort : Class >-> Sortclass.
Arguments op [_] _.
Section Section.
Context (A B: Class) (a: A).
Goal op a || ~~ op a.
by case: op.
Abort.
End Section.
|
