diff options
Diffstat (limited to 'test-suite/modules/PO.v')
| -rw-r--r-- | test-suite/modules/PO.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 71d33177..6198f29a 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -27,13 +27,13 @@ Module Pair (X: PO) (Y: PO) <: PO. Qed. Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3. - unfold le in |- *; intuition; info eauto. + unfold le; intuition; info eauto. Qed. Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2. destruct p1. destruct p2. - unfold le in |- *. + unfold le. intuition. cutrewrite (t = t1). cutrewrite (t0 = t2). |