| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-11 | Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right ↵ | Maxime Dénès | |
| artificially restricted to a non-empty context). | |||
| 2017-09-07 | Merge PR #997: coqdoc: Support comments in verbatim output | Maxime Dénès | |
| 2017-09-04 | fix test-suite/coq-makefile/findlib-package on windows | Enrico Tassi | |
| 2017-09-03 | Addressing BZ#5713 (classical_left/classical_right artificially restricted). | Hugo Herbelin | |
| As explained in BZ#5713 report, the requirement for a non-empty context is not needed, so we remove it. | |||
| 2017-08-31 | Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projections | Maxime Dénès | |
| 2017-08-31 | Merge PR #995: Program: fix BZ#5683, missing lift when building case predicate | Maxime Dénès | |
| 2017-08-31 | Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flag | Maxime Dénès | |
| 2017-08-31 | Merge PR #958: coq_makefile: build/use .cma for packed plugins too | Maxime Dénès | |
| 2017-08-30 | Merge PR #998: Avoid running interactive tests on Windows. | Maxime Dénès | |
| 2017-08-30 | Fixing part of #5707 (allowing destruct to use non dependent case analysis). | Hugo Herbelin | |
| 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. | |||
| 2017-08-29 | coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs | Enrico Tassi | |
| 2017-08-29 | Avoid running interactive tests on Windows. | Maxime Dénès | |
| This is a temporary workaround, until we fix the underlying issue which makes coqtop hang on those tests. | |||
| 2017-08-29 | Properly handling parameters of primitive projections in cctac. | Pierre-Marie Pédrot | |
| 2017-08-29 | Fix BZ#5697: Congruence does not work with primitive projections. | Pierre-Marie Pédrot | |
| The code generating the projection was unconditionally generating pattern-matchings, although this is incorrect for primitive records. | |||
| 2017-08-29 | Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵ | Maxime Dénès | |
| restructuration | |||
| 2017-08-29 | Merge PR #830: Moving assert (the "Cut" rule) to new proof engine | Maxime Dénès | |
| 2017-08-29 | Merge PR #773: [flags] Remove XML output flag. | Maxime Dénès | |
| 2017-08-29 | coq_makefile: use dedicated variable for extra packages | Enrico Tassi | |
| 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. | |||
| 2017-08-29 | coq_makefile: test using findlib's package | Enrico Tassi | |
| 2017-08-29 | coqdoc: Support comments in verbatim output | Tej Chajed | |
| Fixes BZ#5700 | |||
| 2017-08-29 | Adding a test for #5569 (warning about skipping spaces). | Hugo Herbelin | |
| The two previous commits make the warning irrelevant and useless. | |||
| 2017-08-29 | Dropping former fix to bug #5469 (notation format not recognizing curly braces). | Hugo Herbelin | |
| 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. | |||
| 2017-08-29 | A little reorganization of notations + a fix to #5608. | Hugo Herbelin | |
| - 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. | |||
| 2017-08-25 | primproj: fix bug 5245, hnf on proj with simpl never flag. | Matthieu Sozeau | |
| 2017-08-24 | Program: fix BZ#5683, missing lift when building case predicate | Matthieu Sozeau | |
| 2017-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin | |
| 2017-08-21 | Fix coqdoc test-suite target on Windows. | Théo Zimmermann | |
| 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. | |||
| 2017-08-21 | Fixing another regression with 8.4 wrt to βι-normalization of created hyps. | Hugo Herbelin | |
| This one is a continuation of e2a8edaf59 which was βι-normalizing the hypotheses created by a "match". We forgot to do it for "let" and "if". This is what this commit is doing. | |||
| 2017-08-21 | Fixing a new regresssion with 8.4 wrt to βι-normalization of created hyps. | Hugo Herbelin | |
| Formerly, mk_refgoals in logic.ml was applying full βι on new Meta-based goals. We simulate part of this βι-normalization in pose_all_metas_as_evars. I suspect that we don't βι-normalize goals more than in 8.4 by doing that, since all Metas would have eventually gone to mk_refgoals, but difficult to know for sure as there were probably metas turned to evars (and hence a priori not βι-normalized) even when logic.ml was used more pervasively. However, βι-normalizing is a priori a better heuristic than no βι-normalizing, independently of what it was in 8.4 and before (even if, ideally, I would personally lean towards preferring a "chirurgical" substitution with reduction only at the place of substitution). | |||
| 2017-08-16 | Merge PR #942: solving b1859 | Maxime Dénès | |
| 2017-08-16 | Merge PR #954: Print names of all open blocks | Maxime Dénès | |
| 2017-08-16 | Merge PR #841: Timorous fix of bug #5598 on global existing class in sections | Maxime Dénès | |
| 2017-08-16 | Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵ | Maxime Dénès | |
| wrongly tagged as keywords | |||
| 2017-08-16 | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | |
| 2017-08-15 | Adding a test for BZ#1859 as suggested by @tchajed. | Théo Zimmermann | |
| 2017-08-06 | Print names of all open blocks | Tej Chajed | |
| Fixes bug 5597. | |||
| 2017-08-01 | [flags] Remove XML output flag. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-08-01 | Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas). | Maxime Dénès | |
| 2017-08-01 | Merge PR #926: test-suite uses Extraction TestCompile | Maxime Dénès | |
| 2017-08-01 | Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709) | Maxime Dénès | |
| 2017-08-01 | Merge PR #834: Adding support for recursive notations of the form "x , .. , ↵ | Maxime Dénès | |
| y , z". | |||
| 2017-07-31 | Change the option for cumulativity | Amin Timany | |
| 2017-07-31 | Add Jason's example of fun-ext with cumulativity | Amin Timany | |
| 2017-07-31 | Add test for NonCumulative inductives | Amin Timany | |
| 2017-07-31 | Issue error on monomorphic cumulative inductives | Amin Timany | |
| 2017-07-29 | closing bug 5315 | Julien Forest | |
| 2017-07-27 | Fixing bug #5671 (specialize unclean wrt Metas). | Hugo Herbelin | |
| 2017-07-27 | test-suite: more use of the new command Extraction TestCompile | Pierre Letouzey | |
| 2017-07-26 | Fix TypeclassDebug.out after conflicting PR merges | Matthieu Sozeau | |
| 2017-07-26 | test-suite/success/extraction.v : add some Extraction TestCompile | Pierre Letouzey | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite