| Commit message (Expand) | Author | Age |
|---|
| * | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) |  Enrico Tassi | 2015-03-11 |
| * | Do not display the status of monomorphic constants unless in universe-polymor... |  Guillaume Melquiond | 2015-03-09 |
| * | Test for bug #2951. |  Pierre-Marie Pédrot | 2015-03-08 |
| * | Fixing bug #2951. | Pierre-Marie Pédrot | 2015-03-08 |
| * | Test for #4035 (dependent destruction from Ltac). |  Hugo Herbelin | 2015-03-07 |
| * | Reverting r10021 which enforces early assumptions on freshness which | Hugo Herbelin | 2015-03-07 |
| * | Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar". | Hugo Herbelin | 2015-03-07 |
| * | Add some missing Proof keywords. | Guillaume Melquiond | 2015-03-06 |
| * | Simplify grammar for syntax highlighting by removing extraneous parentheses. | Guillaume Melquiond | 2015-03-06 |
| * | Fix syntax highlighting of Print/Reset Extraction. | Guillaume Melquiond | 2015-03-06 |
| * | Fix syntax highlighting of Extraction Inline and add Separate Extraction. | Guillaume Melquiond | 2015-03-06 |
| * | Fix syntax highlighting of Extraction Language. | Guillaume Melquiond | 2015-03-06 |
| * | Fix syntax highlighting of Typeclasses Opaque. | Guillaume Melquiond | 2015-03-06 |
| * | Fix syntax highlighting of Module (Type). | Guillaume Melquiond | 2015-03-06 |
| * | Fix syntax highlighting of Extract Inductive. | Guillaume Melquiond | 2015-03-06 |
| * | Add syntax highlighting for Declare Module. | Guillaume Melquiond | 2015-03-06 |
| * | Fix syntax highlighting of Import and Export. | Guillaume Melquiond | 2015-03-06 |
| * | Add syntax highlighting for Declare ML Module. | Guillaume Melquiond | 2015-03-06 |
| * | Fix syntax highlighting of Require. | Guillaume Melquiond | 2015-03-06 |
| * | Fix syntax highlighting of Scheme. | Guillaume Melquiond | 2015-03-06 |
| * | Do not highlight "using" as a constr keyword. | Guillaume Melquiond | 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-06 |
| * | 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-05 |
| * | Introducing MMaps, a modernized FMaps. | Pierre Letouzey | 2015-03-04 |
| * | Fix bug #3532, providing universe inconsistency information when a |  Matthieu Sozeau | 2015-03-04 |
| * | 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 |
Enrico Tassi
Guillaume Melquiond
Pierre-Marie Pédrot
Hugo Herbelin
Pierre Letouzey
Matthieu Sozeau
Bruno Barras
Pierre Boutillier
mlasson