diff options
| author | Pierre-Marie Pédrot | 2020-06-11 13:03:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-11 13:03:30 +0200 |
| commit | 5611f23271be3c23761450679374690805bf51bb (patch) | |
| tree | 1b886b92a0d1eac35ed95e56ff8a2c6cafbff0b1 /test-suite/modules | |
| parent | c077db40a204132eda8a5d5979022f4961503cab (diff) | |
| parent | 044f76cf32080f0a56309544e5335e44f89725b4 (diff) | |
Merge PR #12423: Remove info tactic, deprecated in 8.5
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite/modules')
| -rw-r--r-- | test-suite/modules/PO.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 4c0ee1b5bd..767b3c1922 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -23,11 +23,11 @@ Module Pair (X: PO) (Y: PO) <: PO. Hint Unfold le. Lemma le_refl : forall p : T, le p p. - info auto. + auto. Qed. Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3. - unfold le; intuition; info eauto. + unfold le; intuition; eauto. Qed. Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2. @@ -39,9 +39,9 @@ Module Pair (X: PO) (Y: PO) <: PO. enough (t0 = t2) as ->. reflexivity. - info auto. + auto. - info auto. + auto. Qed. End Pair. @@ -53,5 +53,5 @@ Require Nat. Module NN := Pair Nat Nat. Lemma zz_min : forall p : NN.T, NN.le (0, 0) p. - info auto with arith. + auto with arith. Qed. |