coq/test-suite/bugs/opened/shouldnotfail, branch master

Testsuite: flatten the 'bugs/opened' directory.

2013-11-29T09:13:20+00:00

Use "Fail" rather than rely on exit code.

2013-09-20T09:34:06+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7

Unset Asymmetric Patterns

2013-01-18T15:21:02+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7

Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"

2010-06-13T11:09:55+00:00

by a regular error in v8.3.
Example behaves better in trunk thanks to new proof engine. In fact,
there are two distinct solutions to a unification problem: should
"refine" commit to one of them or leave the problem open? For trunk,
improved the unification error message by enforcing nf_evar (but at
some time, nf_evar in error messages should move to himsg because it
is costly when errors are used for backtracking).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13127 85f007b7-540e-0410-9357-904b9bb8a0f7

Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which

2010-04-07T22:01:23+00:00

was actually failing for another reason than the reason originally
filled in the bug tracker) and revealed a bug in the unification.v
test file.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12906 85f007b7-540e-0410-9357-904b9bb8a0f7

Delete trailing whitespaces in all .{v,ml} files

2009-09-17T15:58:14+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7

Uniformisation du format des messages d'erreur (commencent par une

2008-07-17T08:35:58+00:00

majuscule - si pas un ident ou un terme - et se terminent par un point).
Restent quelques utilisations de "error" qui sont liées à des usages internes,
ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ?



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7

Temporarily disabling automatic test for bug 1338.v

2008-06-03T06:41:48+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11041 85f007b7-540e-0410-9357-904b9bb8a0f7

Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757

2008-05-07T09:20:43+00:00

+ un error qui devrait être un anomaly


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10893 85f007b7-540e-0410-9357-904b9bb8a0f7

Bug squashing day !

2008-04-17T19:00:55+00:00

- Closed bugs 121, 1696, 1438, 1425, 1696, 1604, 1738, 1760, 1683 related to
setoids. Add corresponding test files.
- Add new modulo_zeta flag to control zeta during unification (e.g. not
allowed for setoid_rewrite unification, but ok for almost everything
else).
- Various fixes in class_tactics with respect to evars and error
messages.
- Correct error message for NoOccurenceFound, distinguishing between a
rewrite in the goal or an hypothesis.
- Move notations for ==>, --> and ++> to level 90 as suggested by
Russell O'Conor.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10813 85f007b7-540e-0410-9357-904b9bb8a0f7