| Age | Commit message (Expand) | Author |
|---|
| 2015-12-17 | CLEANUP: in the Reduction module | Matej Kosik |
| 2015-12-17 | CLEANUP: in the Reductionops module | Matej Kosik |
| 2015-12-17 | CLEANUP: in the Reduction module | Matej Kosik |
| 2015-12-17 | Getting rid of some hardwired generic arguments. | Pierre-Marie Pédrot |
| 2015-12-15 | Fixing e3cefca41b about supposingly simplifying primitive projections | Hugo Herbelin |
| 2015-12-15 | Fixing unexpected length of context in a typing function, detected by | Hugo Herbelin |
| 2015-12-15 | Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite. | Hugo Herbelin |
| 2015-12-15 | API: documenting context_chop and removing a duplicate. | Hugo Herbelin |
| 2015-12-15 | Adding a token "index" representing positions (1st, 2nd, etc.). | Hugo Herbelin |
| 2015-12-15 | Simplifying documentation of "assert form as pat". | Hugo Herbelin |
| 2015-12-15 | Granting clear_flag in injection, even legacy mode. This is possible | Hugo Herbelin |
| 2015-12-15 | Tactics: Generalizing the use of the experimental clearing modifier to | Hugo Herbelin |
| 2015-12-15 | Revert "Revert PMP's fix of #2498, which introduces an incompatibility with l... | Pierre-Marie Pédrot |
| 2015-12-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-12-14 | Extraction: allow basic beta-reduction even through a MLmagic (fix #2795) | Pierre Letouzey |
| 2015-12-14 | Fixing little bug of coq_makefile with unterminated comment. | Hugo Herbelin |
| 2015-12-14 | extraction_impl.v: fix a typo | Pierre Letouzey |
| 2015-12-14 | A test file for Extraction Implicit (including bugs #4243 and #4228) | Pierre Letouzey |
| 2015-12-14 | Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2) | Pierre Letouzey |
| 2015-12-14 | Adding compatibility flag for 8.5. | Hugo Herbelin |
| 2015-12-14 | Fix \label which was meants to be \ref in doc of CIC terms. | Maxime Dénès |
| 2015-12-14 | Remove a mention of Set Virtual Machine in doc. | Maxime Dénès |
| 2015-12-14 | CoqIDE: add 'you need to restart CoqIDE after changing shortcuts' message | Enrico Tassi |
| 2015-12-14 | Updating CHANGES with an incompatibility. | Hugo Herbelin |
| 2015-12-14 | Revert PMP's fix of #2498, which introduces an incompatibility with lablgtk | Maxime Dénès |
| 2015-12-14 | Flag -compat 8.4 now loads Coq.Compat.Coq84. | Maxime Dénès |
| 2015-12-14 | Moved proof_admitted to its own file, named "AdmitAxiom.v". | Maxime Dénès |
| 2015-12-14 | Test file for #4363 was not complete. | Maxime Dénès |
| 2015-12-14 | Extraction: cosmetically avoid generating spaces on empty lines | Pierre Letouzey |
| 2015-12-14 | Remove some occurrences of Unix.opendir. | Guillaume Melquiond |
| 2015-12-14 | Extraction: also get rid of explicit '\n' for haskell | Pierre Letouzey |
| 2015-12-14 | Extraction: fix a pretty-print issue | Pierre Letouzey |
| 2015-12-14 | Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase") | Pierre Letouzey |
| 2015-12-13 | More code sharing between tactic notation and genarg interpretation. | Pierre-Marie Pédrot |
| 2015-12-12 | Extraction: documentation of the new option Unset Extraction SafeImplicits | Pierre Letouzey |
| 2015-12-12 | Extraction: nicer implementation of Implicits | Pierre Letouzey |
| 2015-12-12 | Extraction: check for remaining implicits after dead code removal (fix #4243) | Pierre Letouzey |
| 2015-12-12 | Extraction: fix for bug #4334 (use of delta_resolver in Extract_env) | Pierre Letouzey |
| 2015-12-12 | Extraction: avoid generating some blanks at end-of-line | Pierre Letouzey |
| 2015-12-12 | Removing dead unsafe code in Genarg. | Pierre-Marie Pédrot |
| 2015-12-12 | Indexing and documenting some options. | Pierre-Marie Pédrot |
| 2015-12-11 | Optimize occur_evar_upto_types, avoiding repeateadly looking into the | Matthieu Sozeau |
| 2015-12-11 | Univs: Fix bug #4363, nested abstract. | Matthieu Sozeau |
| 2015-12-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-12-11 | Document removal of Set Virtual Machine and -vm in CHANGES. | Maxime Dénès |
| 2015-12-11 | Remove Set Virtual Machine from doc, since the command itself has been removed. | Maxime Dénès |
| 2015-12-11 | Add tactic native_cast_no_check, analog to vm_cast_no_check. | Maxime Dénès |
| 2015-12-10 | Fixing a pat%constr bug. Thanks to Enrico for reporting. | Hugo Herbelin |
| 2015-12-10 | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | Hugo Herbelin |
| 2015-12-10 | Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removing | Hugo Herbelin |
