Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | * | | | | | primproj: fix bug 5245, hnf on proj with simpl never flag. | Matthieu Sozeau | 2017-08-25 | |
| | | |/ / / / / | ||||
| | | | * / / / | Program: fix BZ#5683, missing lift when building case predicate | Matthieu Sozeau | 2017-08-24 | |
| | | |/ / / / | ||||
| | | | | * / | 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 | 2017-08-21 | |
| |_|/ / / |/| | | | | ||||
* | | | | | 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 wr... | Maxime Dénès | 2017-08-16 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | 2017-08-16 | |
|\ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | Adding a test for BZ#1859 as suggested by @tchajed. | Théo Zimmermann | 2017-08-15 | |
| | | | * | | | | | | Print names of all open blocks | Tej Chajed | 2017-08-06 | |
| |_|_|/ / / / / / |/| | | | | | | | | ||||
| | | | | * | | | | [flags] Remove XML output flag. | Emilio Jesus Gallego Arias | 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 , .. , y... | Maxime Dénès | 2017-08-01 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | | | 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-31 | |
| | | | | | |_|/ / / / | | | | | |/| | | | | | ||||
* | | | | / | | | | | | closing bug 5315 | Julien Forest | 2017-07-29 | |
| |_|_|_|/ / / / / / |/| | | | | | | | | | ||||
| | | | * | | | | | | 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-27 | |
* | | | | | | | | | Fix TypeclassDebug.out after conflicting PR merges | Matthieu Sozeau | 2017-07-26 | |
| |_|_|_|_|_|_|/ |/| | | | | | | | ||||
| | | * | | | | | test-suite/success/extraction.v : add some Extraction TestCompile | Pierre Letouzey | 2017-07-26 | |
| | | * | | | | | Enrich test file 4720.v with a compilation test of the extracted code | Pierre Letouzey | 2017-07-26 | |
| |_|/ / / / / |/| | | | | | | ||||
| | * | | | | | adding a test-suite file 4709.v (thanks to the new command Extraction TestCom... | Pierre Letouzey | 2017-07-26 | |
| |/ / / / / |/| | | | | | ||||
* | | | | | | Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844... | Maxime Dénès | 2017-07-26 | |
|\ \ \ \ \ \ | ||||
| | * | | | | | Adding support for recursive notations of the form "x , .. , y , z". | Hugo Herbelin | 2017-07-26 | |
| |/ / / / / |/| | | | | | ||||
* | | | | | | Merge PR #857: Extraction: various fixes related with bug 4720 | Maxime Dénès | 2017-07-26 | |
|\ \ \ \ \ \ | ||||
| | * | | | | | Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484... | Pierre Letouzey | 2017-07-25 | |
| |/ / / / / |/| | | | | | ||||
| * | | | | | Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720) | Pierre Letouzey | 2017-07-20 | |
* | | | | | | fake_ide: do as coqide to find out coqtop path | Enrico Tassi | 2017-07-20 | |
* | | | | | | more verbose logs for coq-makefile | Enrico Tassi | 2017-07-20 | |
* | | | | | | coq-makefile: make test suite detect more errors | Enrico Tassi | 2017-07-20 | |
* | | | | | | Remove trailing CR before diff in output and misc tests. | Maxime Dénès | 2017-07-20 | |
* | | | | | | Print failure logs on appveyor. | Maxime Dénès | 2017-07-20 | |
* | | | | | | Remove non-terminating Timeout tests from Hints.v. | Maxime Dénès | 2017-07-20 | |
* | | | | | | Make coqlib relative in test suite (revert 024a7ab20b0) | Maxime Dénès | 2017-07-20 | |
|/ / / / / | ||||
* | | | | | Merge PR #869: Enforce alternating separators in typeclass debug output | Maxime Dénès | 2017-07-20 | |
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge branch 'v8.7' | Maxime Dénès | 2017-07-20 | |
|\ \ \ \ \ \ | ||||
| | | * | | | | Removing testing unsupported Next. | Hugo Herbelin | 2017-07-19 | |
| * | | | | | | Merge PR #745: Add timing scripts | Maxime Dénès | 2017-07-19 | |
| |\ \ \ \ \ \ | ||||
| | | | * | | | | Adding a coqdoc target to test-suite. | Hugo Herbelin | 2017-07-17 | |
* | | | | | | | | Getting rid of abstraction breaking code in tclABSTRACT. | Pierre-Marie Pédrot | 2017-07-14 | |
* | | | | | | | | Removing the uses of abstraction-breaking code in Lemmas. | Pierre-Marie Pédrot | 2017-07-13 | |
| |_|_|/ / / / |/| | | | | | | ||||
* | | | | | | | Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel | Maxime Dénès | 2017-07-13 | |
|\ \ \ \ \ \ \ | ||||
| | | | * | | | | format pairs of items for pr_depth to get alternating separators | Paul Steckler | 2017-07-12 | |
| |_|_|/ / / / |/| | | | | | | ||||
| | * | | | | | Deprecate options that were introduced for compatibility with 8.5. | Théo Zimmermann | 2017-07-11 | |
| |/ / / / / |/| | | | | | ||||
| * | | | | | Fix nonsensical universe abstraction in the kernel. | Pierre-Marie Pédrot | 2017-07-11 |