aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/ideal-features
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/ideal-features')
-rw-r--r--test-suite/ideal-features/eapply_evar.v2
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 547860bf1..bb61afb88 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.