diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ideal-features/eapply_evar.v | 2 | ||||
| -rw-r--r-- | test-suite/success/Case3.v (renamed from test-suite/ideal-features/Case3.v) | 0 |
2 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 8c9a448e76..547860bf14 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; diff --git a/test-suite/ideal-features/Case3.v b/test-suite/success/Case3.v index de7784aec5..de7784aec5 100644 --- a/test-suite/ideal-features/Case3.v +++ b/test-suite/success/Case3.v |