aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* An optimization of tactic constructor.Gravatar Hugo Herbelin2017-09-19
| | | | | | | | | As was questioned on Stack Overflow and discussed on Gitter, reduction of the conclusion of the goal was done up to n+1 times for a failing call to "constructor" on an inductive type of n constructors. We do it at most once. Reworking the layout of the code at the same time.
* Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Maxime Dénès2017-09-19
|\
* \ Merge PR #920: kernel: bugfix in filter_stack_domain.Gravatar Maxime Dénès2017-09-19
|\ \
| * | Add test-suite script by Cyprien ManginGravatar Matthieu Sozeau2017-09-18
| | |
* | | Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ | | | | | | | | | | | | Inductive-keyworded record failing even on non-dependent goal)
* \ \ \ Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ | | | | | | | | | | | | | | | work better on them
* \ \ \ \ Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | anonymous variables)
| | | | | * Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Guillaume Melquiond2017-09-14
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This changes the implementation of "constructor" from constructor 1 + ... + constructor n + fail to constructor 1 + ... + constructor n.
* | | | | Fixing bug #5693 (treating empty notation format as any format).Gravatar Hugo Herbelin2017-09-12
| | | | | | | | | | | | | | | | | | | | | | | | | A trick in counting spaces in a format was making the empty notation not behaving correctly.
* | | | | Fixing a bug of recursive notations introduced in dfdaf4de.Gravatar Hugo Herbelin2017-09-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When a proper notation variable occurred only in a recursive pattern of the notation, the notation was wrongly considered non printable due (the side effect that function compare_glob_constr and that mk_glob_constr_eq does not do anymore was indeed done by aux' but thrown away). This fixes it.
* | | | | Fixing little inaccuracy in coercions to ident or name.Gravatar Hugo Herbelin2017-09-12
| | | | | | | | | | | | | | | | | | | | For instance, we don't want "id@{u}" to be coerced to id, or "?[n]" to "_".
* | | | | Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right ↵Gravatar Maxime Dénès2017-09-11
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | artificially restricted to a non-empty context).
* \ \ \ \ \ Merge PR #997: coqdoc: Support comments in verbatim outputGravatar Maxime Dénès2017-09-07
|\ \ \ \ \ \
* | | | | | | fix test-suite/coq-makefile/findlib-package on windowsGravatar Enrico Tassi2017-09-04
| | | | | | |
| | * | | | | Addressing BZ#5713 (classical_left/classical_right artificially restricted).Gravatar Hugo Herbelin2017-09-03
| |/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | As explained in BZ#5713 report, the requirement for a non-empty context is not needed, so we remove it.
* | | | | | Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projectionsGravatar Maxime Dénès2017-08-31
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #995: Program: fix BZ#5683, missing lift when building case predicateGravatar Maxime Dénès2017-08-31
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flagGravatar Maxime Dénès2017-08-31
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #958: coq_makefile: build/use .cma for packed plugins tooGravatar Maxime Dénès2017-08-31
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #998: Avoid running interactive tests on Windows.Gravatar Maxime Dénès2017-08-30
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | Fixing part of #5707 (allowing destruct to use non dependent case analysis).Gravatar Hugo Herbelin2017-08-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The fix covers the case of a non-dependent goal with unavailable dependent case analysis: destruct was not seeing that it could still use non-dependent case analysis.
| | * | | | | | | | | coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxsGravatar Enrico Tassi2017-08-29
| | | | | | | | | | |
| * | | | | | | | | | Avoid running interactive tests on Windows.Gravatar Maxime Dénès2017-08-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a temporary workaround, until we fix the underlying issue which makes coqtop hang on those tests.
| | | | | * | | | | | Properly handling parameters of primitive projections in cctac.Gravatar Pierre-Marie Pédrot2017-08-29
| | | | | | | | | | |
| | | | | * | | | | | Fix BZ#5697: Congruence does not work with primitive projections.Gravatar Pierre-Marie Pédrot2017-08-29
| |_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The code generating the projection was unconditionally generating pattern-matchings, although this is incorrect for primitive records.
* | | | | | | | | | Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵Gravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | restructuration
* \ \ \ \ \ \ \ \ \ \ Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / |/| | | | | | | | | | |
| | | | * | | | | | | | coq_makefile: use dedicated variable for extra packagesGravatar Enrico Tassi2017-08-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CAMLPKGS is now used to hold extra findlib -packages The previous solution was to use CAMLFLAGS but since 4.05 an invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx` fails saying that `useless.cmxa` is not a compilation unit description. CAMLPKGS is used in all `ocamlopt` invocations but for the one performing the packing.
| | | | * | | | | | | | coq_makefile: test using findlib's packageGravatar Enrico Tassi2017-08-29
| |_|_|/ / / / / / / / |/| | | | | | | | | |
| | | | | | * | | | | coqdoc: Support comments in verbatim outputGravatar Tej Chajed2017-08-29
| | | | | | | |_|/ / | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | Fixes BZ#5700
| | | * | | | | | | Adding a test for #5569 (warning about skipping spaces).Gravatar Hugo Herbelin2017-08-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The two previous commits make the warning irrelevant and useless.
| | | * | | | | | | Dropping former fix to bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-08-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 53a50875 and a bit more: it also makes the check for possibly ignoring formatting spaces irrelevant, since the previous commit makes that curly brackets are not any more dropped for printing.
| | | * | | | | | | A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
| | | | |_|/ / / / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation.
| | | | * | | | | primproj: fix bug 5245, hnf on proj with simpl never flag.Gravatar Matthieu Sozeau2017-08-25
| | | |/ / / / /
| | | | * / / / Program: fix BZ#5683, missing lift when building case predicateGravatar Matthieu Sozeau2017-08-24
| | | |/ / / /
| | | | | * / Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
| | | | |/ / | | | |/| |
* | | / | | Fix coqdoc test-suite target on Windows.Gravatar Théo Zimmermann2017-08-21
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | Commit 8f12597 introduced new output tests but these were broken on Windows. We fix them by using --strip-trailing-cr option of diff, like in other output tests in the test-suite.
* | | | | Merge PR #942: solving b1859Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \
* \ \ \ \ \ Merge PR #954: Print names of all open blocksGravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsGravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | wrongly tagged as keywords
* \ \ \ \ \ \ \ \ Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \ \
| | | | | * | | | | Adding a test for BZ#1859 as suggested by @tchajed.Gravatar Théo Zimmermann2017-08-15
| | | | | | | | | |
| | | | * | | | | | Print names of all open blocksGravatar Tej Chajed2017-08-06
| |_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | Fixes bug 5597.
| | | | | * | | | [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| |_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
* | | | | | | | Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #926: test-suite uses Extraction TestCompileGravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #834: Adding support for recursive notations of the form "x , .. , ↵Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | y , z".
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 14:55:25 +0000