| Age | Commit message (Expand) | Author |
|---|
| 2015-03-06 | Add syntax highlighting for About. | Guillaume Melquiond |
| 2015-03-06 | Fix syntax highlighting of Save. | Guillaume Melquiond |
| 2015-03-06 | Fix syntax highlighting of Hypothesis, Axiom, Variable, Parameter, and Context. | Guillaume Melquiond |
| 2015-03-06 | Add syntax highlighting for Coercion. | Guillaume Melquiond |
| 2015-03-06 | Fix syntax highlighting of "Require multiple libraries". | Guillaume Melquiond |
| 2015-03-06 | MMapPositive: another implementation of MMaps | Pierre Letouzey |
| 2015-03-05 | Fix testsuite with respect to the new formatting of Fail messages. | Guillaume Melquiond |
| 2015-03-05 | Preprend Fail to all the expected failures in the documentation. | Guillaume Melquiond |
| 2015-03-05 | Do not prepend a "Error:" header when the error is expected by the user. | Guillaume Melquiond |
| 2015-03-05 | MMaps again : adding MMapList, an implementation by ordered list | Pierre Letouzey |
| 2015-03-04 | Introducing MMaps, a modernized FMaps. | Pierre Letouzey |
| 2015-03-04 | Fix bug #3532, providing universe inconsistency information when a | Matthieu Sozeau |
| 2015-03-03 | Fix test-suite file, this is open. | Matthieu Sozeau |
| 2015-03-03 | Fix bug #3732: firstorder was using detyping to build existential | Matthieu Sozeau |
| 2015-03-03 | Add missing test-suite files and update gitignore. | Matthieu Sozeau |
| 2015-03-03 | Add a test-suite file ensuring coinductives with primitive projections | Matthieu Sozeau |
| 2015-03-03 | Fix test-suite file, this is currently a wontfix, but keep the | Matthieu Sozeau |
| 2015-03-03 | Fix bug #3590, keeping evars that are not turned into named metas by | Matthieu Sozeau |
| 2015-03-03 | Improving display of camlp4/camlp5 versions, library and binary locations. | Hugo Herbelin |
| 2015-03-03 | Reinstalling search of camlpX in camldir, when given, for | Hugo Herbelin |
| 2015-03-03 | Typos in doc modules. | Hugo Herbelin |
| 2015-03-03 | Fix bug #4103: forgot to allow unfolding projections of cofixpoints like | Matthieu Sozeau |
| 2015-03-03 | Fix bug #4101, noccur_evar's expand_projection can legitimately fail | Matthieu Sozeau |
| 2015-03-03 | Fix bug introduced by my last commit, forgetting to adjust de Bruijn | Matthieu Sozeau |
| 2015-03-02 | Fix bug #4097. | Matthieu Sozeau |
| 2015-03-02 | Now accepting unit props in mutual definitions | Bruno Barras |
| 2015-02-28 | Coq_makefile clean target erases .coq-native dirs in . if they are empty | Pierre Boutillier |
| 2015-02-28 | Fixing the rule for ml4 depencies in coq_makefile | mlasson |
| 2015-02-28 | Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ... | Pierre Boutillier |
| 2015-02-27 | Adding a test for bug #3612. | Pierre-Marie Pédrot |
| 2015-02-27 | Removing the unused field ltacrecvars of tactic internalization. | Pierre-Marie Pédrot |
| 2015-02-27 | Fixing OCaml 3.12 compilation. | Pierre-Marie Pédrot |
| 2015-02-27 | Test for bug #3249. | Pierre-Marie Pédrot |
| 2015-02-27 | Fixing bug #3249. | Pierre-Marie Pédrot |
| 2015-02-27 | Taking current env and not global env in b286c9f4f42f (4 commits ago, | Hugo Herbelin |
| 2015-02-27 | simpl: honor Global for "simpl: never" (Close: 3206) | Enrico Tassi |
| 2015-02-27 | STM: Considering Stack_overflow as a normal tactic error (Close #3576) | Enrico Tassi |
| 2015-02-27 | Fix test for #3467, I had moved it in a dumb way. | Maxime Dénès |
| 2015-02-27 | Add support so that the type of a match in an inductive type with let-in | Hugo Herbelin |
| 2015-02-27 | Hack so that refine_no_check accepts an argument which is a match on an | Hugo Herbelin |
| 2015-02-27 | Fixing first part of bug #3210 (inference of pattern-matching return | Hugo Herbelin |
| 2015-02-27 | Fixing typo resulting in wrong printing of return clauses for | Hugo Herbelin |
| 2015-02-27 | Fix test for #3848, still open. | Maxime Dénès |
| 2015-02-27 | Moving test for #3467 to closed after PMP's fix. | Maxime Dénès |
| 2015-02-27 | Fix test-suite files for bugs #2456 and #3593, still open. | Maxime Dénès |
| 2015-02-27 | Make coq_makefile generate double-colon rules for clean and archclean. (Fix b... | Guillaume Melquiond |
| 2015-02-27 | Somehow fixing bug #3467. | Pierre-Marie Pédrot |
| 2015-02-27 | Add test-suite file for #3649. | Maxime Dénès |
| 2015-02-27 | Moving tests for #2456 and #3593 to "opened" until they're fixed. | Maxime Dénès |
| 2015-02-27 | Made test for #3392 rely less on unification. | Maxime Dénès |
