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 8c9a448e7..547860bf1 100644 --- a/test-suite/ideal-features/eapply_evar.v +++ b/test-suite/ideal-features/eapply_evar.v @@ -1,7 +1,7 @@ (* Test propagation of evars from subgoal to brother subgoals *) (* This does not work (oct 2008) because "match goal" sees "?evar = O" - and not "O = O" + and not "O = O" *) Lemma eapply_evar : O=O -> 0=O. intro H; eapply trans_equal; |