| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | 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-03 |
| * | Fix bug #4097. | Matthieu Sozeau | 2015-03-02 |
| * | Now accepting unit props in mutual definitions |  Bruno Barras | 2015-03-02 |
| * | 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-28 |
| * | 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 | 2015-02-27 |
| * | Moving test of #3848 to "opened". | Maxime Dénès | 2015-02-27 |
| * | Test for #2602, which seems now fixed. | Maxime Dénès | 2015-02-26 |
| * | Test for bug #3298. | Pierre-Marie Pédrot | 2015-02-26 |
| * | Fixing bug #3298. | Pierre-Marie Pédrot | 2015-02-26 |
| * | Trying to fix code locating camlp4/camlp5. | Maxime Dénès | 2015-02-26 |
| * | Fixing bug 3099. | Pierre-Marie Pédrot | 2015-02-26 |
| * | Fixing printing error in coq_makefile. | Pierre-Marie Pédrot | 2015-02-26 |
| * | Fixing printing of ordinals. | Pierre-Marie Pédrot | 2015-02-26 |
| * | Mention -R option in warnings, fixing #4067 and #4068. | Maxime Dénès | 2015-02-26 |
| * | Fix checker after addition of a universe context in with t := c constraints. | Matthieu Sozeau | 2015-02-26 |
| * | Fixing complexity tests for #4076. | Maxime Dénès | 2015-02-26 |
| * | Revert "Fixing bug #4035 (support for dependent destruction within ltac code)." | Maxime Dénès | 2015-02-26 |
Matthieu Sozeau
Hugo Herbelin
Bruno Barras
Pierre Boutillier
mlasson
Pierre-Marie Pédrot
Enrico Tassi
Maxime Dénès
Guillaume Melquiond