Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | * | | | | | | Properly handling parameters of primitive projections in cctac. | 2017-08-29 | ||
| | | | | * | | | | | | Fix BZ#5697: Congruence does not work with primitive projections. | 2017-08-29 | ||
| |_|_|_|/ / / / / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur... | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #830: Moving assert (the "Cut" rule) to new proof engine | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #773: [flags] Remove XML output flag. | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / |/| | | | | | | | | | | | ||||
| | | | * | | | | | | | | coq_makefile: use dedicated variable for extra packages | 2017-08-29 | ||
| | | | * | | | | | | | | coq_makefile: test using findlib's package | 2017-08-29 | ||
| |_|_|/ / / / / / / / |/| | | | | | | | | | | ||||
| | | | | | * | | | | | coqdoc: Support comments in verbatim output | 2017-08-29 | ||
| | | | | | | |_|/ / | | | | | | |/| | | | ||||
| | | * | | | | | | | Adding a test for #5569 (warning about skipping spaces). | 2017-08-29 | ||
| | | * | | | | | | | Dropping former fix to bug #5469 (notation format not recognizing curly braces). | 2017-08-29 | ||
| | | * | | | | | | | A little reorganization of notations + a fix to #5608. | 2017-08-29 | ||
| | | | |_|/ / / / | | | |/| | | | | | ||||
| | | | * | | | | | primproj: fix bug 5245, hnf on proj with simpl never flag. | 2017-08-25 | ||
| | | |/ / / / / | ||||
| | | | * / / / | Program: fix BZ#5683, missing lift when building case predicate | 2017-08-24 | ||
| | | |/ / / / | ||||
| | | | | * / | Ensuring all .v files end with a newline to make "sed -i" work better on them. | 2017-08-21 | ||
| | | | |/ / | | | |/| | | ||||
* | | / | | | Fix coqdoc test-suite target on Windows. | 2017-08-21 | ||
| |_|/ / / |/| | | | | ||||
* | | | | | Merge PR #942: solving b1859 | 2017-08-16 | ||
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR #954: Print names of all open blocks | 2017-08-16 | ||
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR #841: Timorous fix of bug #5598 on global existing class in sections | 2017-08-16 | ||
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords wr... | 2017-08-16 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #864: Some cleanups after cumulativity for inductive types | 2017-08-16 | ||
|\ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | Adding a test for BZ#1859 as suggested by @tchajed. | 2017-08-15 | ||
| | | | * | | | | | | Print names of all open blocks | 2017-08-06 | ||
| |_|_|/ / / / / / |/| | | | | | | | | ||||
| | | | | * | | | | [flags] Remove XML output flag. | 2017-08-01 | ||
| |_|_|_|/ / / / |/| | | | | | | | ||||
* | | | | | | | | Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas). | 2017-08-01 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #926: test-suite uses Extraction TestCompile | 2017-08-01 | ||
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709) | 2017-08-01 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #834: Adding support for recursive notations of the form "x , .. , y... | 2017-08-01 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | | | Change the option for cumulativity | 2017-07-31 | ||
| | | | | * | | | | | | | Add Jason's example of fun-ext with cumulativity | 2017-07-31 | ||
| | | | | * | | | | | | | Add test for NonCumulative inductives | 2017-07-31 | ||
| | | | | * | | | | | | | Issue error on monomorphic cumulative inductives | 2017-07-31 | ||
| | | | | | |_|/ / / / | | | | | |/| | | | | | ||||
* | | | | / | | | | | | closing bug 5315 | 2017-07-29 | ||
| |_|_|_|/ / / / / / |/| | | | | | | | | | ||||
| | | | * | | | | | | Fixing bug #5671 (specialize unclean wrt Metas). | 2017-07-27 | ||
| |_|_|/ / / / / / |/| | | | | | | | | ||||
| | | * | | | | | | test-suite: more use of the new command Extraction TestCompile | 2017-07-27 | ||
* | | | | | | | | | Fix TypeclassDebug.out after conflicting PR merges | 2017-07-26 | ||
| |_|_|_|_|_|_|/ |/| | | | | | | | ||||
| | | * | | | | | test-suite/success/extraction.v : add some Extraction TestCompile | 2017-07-26 | ||
| | | * | | | | | Enrich test file 4720.v with a compilation test of the extracted code | 2017-07-26 | ||
| |_|/ / / / / |/| | | | | | | ||||
| | * | | | | | adding a test-suite file 4709.v (thanks to the new command Extraction TestCom... | 2017-07-26 | ||
| |/ / / / / |/| | | | | | ||||
* | | | | | | Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844... | 2017-07-26 | ||
|\ \ \ \ \ \ | ||||
| | * | | | | | Adding support for recursive notations of the form "x , .. , y , z". | 2017-07-26 | ||
| |/ / / / / |/| | | | | | ||||
* | | | | | | Merge PR #857: Extraction: various fixes related with bug 4720 | 2017-07-26 | ||
|\ \ \ \ \ \ | ||||
| | * | | | | | Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484... | 2017-07-25 | ||
| |/ / / / / |/| | | | | | ||||
| * | | | | | Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720) | 2017-07-20 | ||
* | | | | | | fake_ide: do as coqide to find out coqtop path | 2017-07-20 | ||
* | | | | | | more verbose logs for coq-makefile | 2017-07-20 | ||
* | | | | | | coq-makefile: make test suite detect more errors | 2017-07-20 | ||
* | | | | | | Remove trailing CR before diff in output and misc tests. | 2017-07-20 | ||
* | | | | | | Print failure logs on appveyor. | 2017-07-20 | ||
* | | | | | | Remove non-terminating Timeout tests from Hints.v. | 2017-07-20 | ||
* | | | | | | Make coqlib relative in test suite (revert 024a7ab20b0) | 2017-07-20 | ||
|/ / / / / |