diff options
Diffstat (limited to 'test-suite/bugs/opened/3295.v')
| -rw-r--r-- | test-suite/bugs/opened/3295.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/3295.v index 2a156e33..c09649de 100644 --- a/test-suite/bugs/opened/3295.v +++ b/test-suite/bugs/opened/3295.v @@ -5,7 +5,7 @@ Class lops := lmk_ops { weq: relation car }. -Implicit Arguments car []. +Arguments car : clear implicits. Coercion car: lops >-> Sortclass. @@ -23,7 +23,7 @@ Class ops := mk_ops { dot: forall n m p, mor n m -> mor m p -> mor n p }. Coercion mor: ops >-> Funclass. -Implicit Arguments ob []. +Arguments ob : clear implicits. Instance dot_weq `{ops} n m p: Proper (weq ==> weq ==> weq) (dot n m p). Proof. |