diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-17 19:04:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-17 19:04:21 +0000 |
| commit | 6022cfa362ec218bda39b0bda7f307e2664c3e26 (patch) | |
| tree | 2962cf083089f177c4f033250a453da6656c4859 /test-suite | |
| parent | 3c73a7b325dfb0bd7634abd0932674ec96479829 (diff) | |
Moved Case3.v from ideal features to success (it works since 8.2).
Two other tests are still "ideal features" though not failing
(evars_subst.v is a complexity test still of bad complexity and
universes.v just describes an improvement to do without checking
anything).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12949 85f007b7-540e-0410-9357-904b9bb8a0f7
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 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; diff --git a/test-suite/ideal-features/Case3.v b/test-suite/success/Case3.v index de7784aec..de7784aec 100644 --- a/test-suite/ideal-features/Case3.v +++ b/test-suite/success/Case3.v |