diff options
Diffstat (limited to 'test-suite/ideal-features/eapply_evar.v')
| -rw-r--r-- | test-suite/ideal-features/eapply_evar.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/ideal-features/eapply_evar.v b/test-suite/ideal-features/eapply_evar.v index 547860bf..bb61afb8 100644 --- a/test-suite/ideal-features/eapply_evar.v +++ b/test-suite/ideal-features/eapply_evar.v @@ -4,6 +4,6 @@ and not "O = O" *) Lemma eapply_evar : O=O -> 0=O. -intro H; eapply trans_equal; +intro H; eapply eq_trans; [apply H | match goal with |- ?x = ?x => reflexivity end]. Qed. |