| Age | Commit message (Expand) | Author |
|---|
| 2015-01-27 | Fixed a wrong warning in coq_makefile. | Pierre Courtieu |
| 2015-01-27 | Allow -type-in-type to be an option also for coqc. | Daniel R. Grayson |
| 2015-01-27 | Doc: Overfull lines in chapter on Canonical Structures. | Hugo Herbelin |
| 2015-01-25 | Made replacing of text in CoqIDE atomic w.r.t. the undo/redo. | Pierre-Marie Pédrot |
| 2015-01-25 | Fixing bug #3947. | Pierre-Marie Pédrot |
| 2015-01-25 | Test for bug #3798. | Pierre-Marie Pédrot |
| 2015-01-24 | Doc: Fixing some compilation problems with chapter Canonical | Hugo Herbelin |
| 2015-01-24 | Updating CHANGES (grammar, thanks to AS for pointing it out) + | Hugo Herbelin |
| 2015-01-24 | Removed obsolete option "Legacy Partially Applied Elimination | Hugo Herbelin |
| 2015-01-24 | Reference Manual: Documenting new printing of evars and new effect of | Hugo Herbelin |
| 2015-01-24 | Equality Schemes options: reverting commit ff9f94634 which is | Hugo Herbelin |
| 2015-01-24 | Isolate a function for printing evar sets. | Hugo Herbelin |
| 2015-01-24 | Tentative workaround for bug #3798. | Pierre-Marie Pédrot |
| 2015-01-23 | Fix previous commit on extraction. | Maxime Dénès |
| 2015-01-23 | Typos, grammar, layout in CHANGES (continued). | Hugo Herbelin |
| 2015-01-23 | Typos, grammar, layout in CHANGES. | Hugo Herbelin |
| 2015-01-23 | Extraction: fix #3629. | Maxime Dénès |
| 2015-01-21 | Add the possibility of defining opaque terms with program. | mlasson |
| 2015-01-21 | Reference Manual/Credits: expand the paragraph on the new proof engine to mat... | Arnaud Spiwack |
| 2015-01-21 | Reference Manual/Credits: native compute is a major contribution. | Arnaud Spiwack |
| 2015-01-21 | Reference manual/Credits: populate the "various smaller-scale improvements" p... | Arnaud Spiwack |
| 2015-01-21 | Reference Manual/Credits: remove a duplicate. | Arnaud Spiwack |
| 2015-01-21 | Reference manual: pass over the credit section for English. | Arnaud Spiwack |
| 2015-01-21 | Reference manual: fix typo in doc of [tryif/then/else]. | Arnaud Spiwack |
| 2015-01-20 | Fix a critical bug in machine arithmetic for native compiler. | Maxime Dénès |
| 2015-01-19 | Making unification of LetIn's expressions more consistent (see #3920). | Hugo Herbelin |
| 2015-01-18 | Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it was | Maxime Dénès |
| 2015-01-17 | Remove dead code. | Maxime Dénès |
| 2015-01-17 | Fix #3379, now that Require inside modules is allowed again. | Maxime Dénès |
| 2015-01-18 | There was one more universe needed due to the use of now non-universe-polymor... | Matthieu Sozeau |
| 2015-01-17 | Back to 4 expected universes. | Matthieu Sozeau |
| 2015-01-17 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau |
| 2015-01-17 | Univs: Complete documentation in refman. | Matthieu Sozeau |
| 2015-01-17 | Partially revert "Forbid Require inside interactive modules and module types." | Maxime Dénès |
| 2015-01-17 | Revert "Adapting two files from test-suite to now forbidden Require's in modu... | Maxime Dénès |
| 2015-01-17 | Revert "Update test for #3363 now that Require is forbidden inside modules." | Maxime Dénès |
| 2015-01-17 | Revert "Fix files in test-suite having to do with Require inside modules." | Maxime Dénès |
| 2015-01-17 | Avoid compilation warning... might not be the best fix though. | Matthieu Sozeau |
| 2015-01-17 | Univs: Fix alias computation for VMs, computation of normal form of | Matthieu Sozeau |
| 2015-01-17 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès |
| 2015-01-16 | coq_makefile: install also .v and .glob | Enrico Tassi |
| 2015-01-16 | Documenting the removal of coercions between sig, sigT, sig2, | Hugo Herbelin |
| 2015-01-16 | Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _" | Matthieu Sozeau |
| 2015-01-15 | vm_printers: fix compilation | Enrico Tassi |
| 2015-01-15 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau |
| 2015-01-15 | Minor fixes to the refman credits to be continued. | Matthieu Sozeau |
| 2015-01-15 | Move explanations about primitive projections to the manual. | Matthieu Sozeau |
| 2015-01-15 | Add a (by default deactivated) option to force typeclass resolution to | Matthieu Sozeau |
| 2015-01-15 | Expand Credits for 8.5 and doc on universes | Matthieu Sozeau |
| 2015-01-15 | Remove typeclass opaque directive, some proofs in the stdlib rely on it being... | Matthieu Sozeau |
