| Age | Commit message (Expand) | Author |
|---|
| 2015-03-13 | CHANGES: more correct equivalent to "constructor tac" syntax. | Arnaud Spiwack |
| 2015-03-13 | Add some tests for tryif | Jason Gross |
| 2015-03-13 | Fixing #4127 (command for locating exists notation in refman changed). | Hugo Herbelin |
| 2015-03-12 | Fixing bug #4055. | Pierre-Marie Pédrot |
| 2015-03-11 | Fix double print in decl_mode. | Enrico Tassi |
| 2015-03-11 | Fix regression in HoTT_coq_014.v | Enrico Tassi |
| 2015-03-11 | CoqIDE: load first _CoqProject file found and notify the user | Enrico Tassi |
| 2015-03-11 | CoqIDE: fix tag colors to support superposing unsafe and partial | Enrico Tassi |
| 2015-03-11 | CoqIDE: restore module/proof name in info bar | Enrico Tassi |
| 2015-03-11 | CoqIDE: do not lose tag on Qed ending focused proof | Enrico Tassi |
| 2015-03-11 | STM: ease re-editing of Admitted proofs | Enrico Tassi |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
| 2015-03-09 | Do not display the status of monomorphic constants unless in universe-polymor... | Guillaume Melquiond |
| 2015-03-08 | Test for bug #2951. | Pierre-Marie Pédrot |
| 2015-03-08 | Fixing bug #2951. | Pierre-Marie Pédrot |
| 2015-03-07 | 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-06 | 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-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 |
