diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/eqdecide.v | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 5f2d0f3954..8c00583ed6 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -16,12 +16,7 @@ Qed. Lemma lem2 : forall x y : T, {x = y} + {x <> y}. intros x y. - decide equality x y. -Qed. - -Lemma lem3 : forall x y : T, {x = y} + {x <> y}. -intros x y. - decide equality y x. + decide equality. Qed. Lemma lem4 : forall x y : T, {x = y} + {x <> y}. |