| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-15 | Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" ↵ | Maxime Dénès | |
| Inductive-keyworded record failing even on non-dependent goal) | |||
| 2017-09-15 | Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵ | Maxime Dénès | |
| work better on them | |||
| 2017-09-15 | Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match ↵ | Maxime Dénès | |
| anonymous variables) | |||
| 2017-09-12 | Fixing bug #5693 (treating empty notation format as any format). | Hugo Herbelin | |
| A trick in counting spaces in a format was making the empty notation not behaving correctly. | |||
| 2017-09-12 | Fixing a bug of recursive notations introduced in dfdaf4de. | Hugo Herbelin | |
| 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. | |||
| 2017-09-12 | Fixing little inaccuracy in coercions to ident or name. | Hugo Herbelin | |
| For instance, we don't want "id@{u}" to be coerced to id, or "?[n]" to "_". | |||
| 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-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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite