| Age | Commit message (Expand) | Author |
|---|
| 2015-08-19 | Documentation by giving a name to a large type. | Pierre-Marie Pédrot |
| 2015-08-17 | Highlighting of the "Next Obligation" command in CoqIDE. | Pierre-Marie Pédrot |
| 2015-08-17 | windows build scripts made more accurate in detecting failures | Enrico Tassi |
| 2015-08-17 | Remove duplicate code. | Guillaume Melquiond |
| 2015-08-17 | Remove generatable documentation files from repository. (Fix bug #4315) | Guillaume Melquiond |
| 2015-08-15 | Revert the four previous commits and update the description of Richpp. | Pierre-Marie Pédrot |
| 2015-08-15 | More invariants in Richpp. | Pierre-Marie Pédrot |
| 2015-08-15 | More parametric type for generalized XML. | Pierre-Marie Pédrot |
| 2015-08-15 | Statically ensure that we omit null annotations in Richpp. | Pierre-Marie Pédrot |
| 2015-08-15 | Fixing richpp behaviour w.r.t. its specification. | Pierre-Marie Pédrot |
| 2015-08-13 | report the full module path when reporting errors in coqdep | Gregory Malecha |
| 2015-08-03 | Test file for #4254: Mutual inductives with parameters on Type raises anomaly. | Maxime Dénès |
| 2015-08-02 | Continuing 817308ab (use ltac env for terms in ltac context) + fix | Hugo Herbelin |
| 2015-08-02 | Fixing test apply.v (had wrong option name). | Hugo Herbelin |
| 2015-08-02 | Fixing pop_rel_context. | Hugo Herbelin |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | Hconsing continued | Hugo Herbelin |
| 2015-08-02 | Fixing test apply.v (had wrong option name). | Hugo Herbelin |
| 2015-08-02 | Fixing pop_rel_context | Hugo Herbelin |
| 2015-08-02 | Documenting in passing. | Hugo Herbelin |
| 2015-08-02 | Hopefully clearer printing of stack when debugging evarconv unification. | Hugo Herbelin |
| 2015-08-02 | Failing when reaching end of file with unterminated comment when | Hugo Herbelin |
| 2015-08-02 | Cosmetic changes in evarconv.ml: hopefully more regular names and form | Hugo Herbelin |
| 2015-08-02 | Cosmetic changes in evarconv.ml: hopefully more regular form and | Hugo Herbelin |
| 2015-08-02 | Cosmetic changes in evarconv.ml: hopefully using better self-documenting names. | Hugo Herbelin |
| 2015-08-02 | Evarconv.ml: small cut-elimination, saving useless zip. | Hugo Herbelin |
| 2015-08-02 | Cosmetic in evarconv.ml: naming a local function for better readibility. | Hugo Herbelin |
| 2015-08-02 | Adding a notation { x & P } for { x : _ & P }. | Hugo Herbelin |
| 2015-08-02 | A patch renaming equal into eq in the module dealing with | Hugo Herbelin |
| 2015-08-02 | Adding eq/compare/hash for syntactic view at | Hugo Herbelin |
| 2015-08-02 | Give a way to control if the decidable-equality schemes are built like | Hugo Herbelin |
| 2015-08-02 | Removing the generalization of the body of inductive schemes from | Hugo Herbelin |
| 2015-08-02 | Fixing #4221 (interpreting bound variables using ltac env was possibly | Hugo Herbelin |
| 2015-08-02 | Granting Jason's request for an ad hoc compatibility option on | Hugo Herbelin |
| 2015-08-02 | Documenting change of behavior of apply when the lemma is a tuple and | Hugo Herbelin |
| 2015-08-02 | For convenience, making yes and on, and no and off synonymous in | Hugo Herbelin |
| 2015-07-31 | Fix typos in the Extraction part of the reference manual. | Guillaume Melquiond |
| 2015-07-31 | Fix typos in the Micromega part of the reference manual. | Guillaume Melquiond |
| 2015-07-31 | Improve the table of content of the reference manual. | Guillaume Melquiond |
| 2015-07-31 | Remove some outdated files and fix permissions. | Guillaume Melquiond |
| 2015-07-30 | Followup of 9f81b58551. | Pierre-Marie Pédrot |
| 2015-07-30 | STM: make multiple, admitted, nested proofs work (fix #4314) | Enrico Tassi |
| 2015-07-30 | STM: emit a warning when a QED/Admitted proof contains a nested lemma | Enrico Tassi |
| 2015-07-30 | STM: fix backtrack in presence of nested, immediate, proofs | Enrico Tassi |
| 2015-07-30 | STM: remove assertion not being true for nested, immediate, proofs (#4313) | Enrico Tassi |
| 2015-07-30 | Test file for bug #4289 (buggy hash-consing of kernel name pairs | Hugo Herbelin |
| 2015-07-30 | Fixing bug #4289 (hash-consing only user part of constant not | Hugo Herbelin |
| 2015-07-30 | A printer for printing constants of the env (maybe useful when there are not ... | Hugo Herbelin |
| 2015-07-30 | Avoid suggesting elim and decompose in the FAQ. | Guillaume Melquiond |
| 2015-07-30 | Remove some output of Qed in the FAQ. | Guillaume Melquiond |
