| Age | Commit message (Expand) | Author |
|---|
| 2016-05-04 | Interpretation function can return any untyped value. | Pierre-Marie Pédrot |
| 2016-05-04 | Removing external uses of Val.inject and making Geninterp.interp return Val.t | Pierre-Marie Pédrot |
| 2016-05-04 | Removing the Value.of_* API for parameterized types. | Pierre-Marie Pédrot |
| 2016-05-04 | Do not generate generic arguments for data which only requires toplevel values. | Pierre-Marie Pédrot |
| 2016-05-04 | More toplevel value representation sharing. | Pierre-Marie Pédrot |
| 2016-05-04 | Moving the Val module to Geninterp. | Pierre-Marie Pédrot |
| 2016-05-04 | Simplifying the code of Tacinterp. | Pierre-Marie Pédrot |
| 2016-05-04 | Getting rid of the Geninterp.generic_interp function. | Pierre-Marie Pédrot |
| 2016-05-04 | Switching to an untyped toplevel representation for Ltac values. | Pierre-Marie Pédrot |
| 2016-05-04 | Moving Ftactic and Geninterp to the engine folder. | Pierre-Marie Pédrot |
| 2016-05-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-05-04 | Int.v: simplify Jason's commit 5b4e3ace | Pierre Letouzey |
| 2016-05-04 | Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int... | Pierre Letouzey |
| 2016-05-04 | Fixing subst.out after changing spacing in goal output (24a125b77). | Hugo Herbelin |
| 2016-05-04 | Fix Haskell extraction for terms over 45 characters long | Nickolai Zeldovich |
| 2016-05-04 | Handle primitive projections inside types when extracting (bug #4616). | Guillaume Melquiond |
| 2016-05-04 | Fix for #4603, part 3: definitions inside proofs not handled properly by coqc. | Maxime Dénès |
| 2016-05-04 | Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into t... | Pierre Letouzey |
| 2016-05-04 | Increase the size of the dumpglob buffer for cooking notations (bug #4708). | Guillaume Melquiond |
| 2016-05-03 | In Regular Subst Tactic mode, ensure that the order of hypotheses is | Hugo Herbelin |
| 2016-05-03 | Fix bug #4707: clearbody much slower in 8.5pl1. | Pierre-Marie Pédrot |
| 2016-05-03 | Fix bug #3825: Universe annotations on notations should pass through or be re... | Pierre-Marie Pédrot |
| 2016-05-03 | Test file for #4695: Slow Qed. | Maxime Dénès |
| 2016-05-03 | Fix bug #4292: Unexpected functor objects. | Pierre-Marie Pédrot |
| 2016-05-03 | Use the canonical name when looking for an eliminator (bug #4670). | Guillaume Melquiond |
| 2016-05-03 | A note concerning the "Drop" command. | Matej Kosik |
| 2016-05-03 | Fix bug #4705: coqtop accepts both -emacs and -ideslave. | Pierre-Marie Pédrot |
| 2016-05-03 | setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug. | Matej Kosik |
| 2016-05-03 | Call hooks when terminating a definition proof (bug #4663). | Guillaume Melquiond |
| 2016-05-03 | Remove extraneous space in coqtop/pg output (bug #4675). | Guillaume Melquiond |
| 2016-05-02 | Make votour a bit more robust/forgiving with respect to user commands (bug #4... | Guillaume Melquiond |
| 2016-05-02 | Properly handle notations containing spaces (bug #4538). | Guillaume Melquiond |
| 2016-05-02 | Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576). | Guillaume Melquiond |
| 2016-05-02 | Generate parsing rules for ML tactics in the same order as before a7917a32. | Pierre-Marie Pédrot |
| 2016-05-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-05-02 | Useless code in Tacentries. | Pierre-Marie Pédrot |
| 2016-04-29 | Reduce ide/coq.png to 256x256. | Guillaume Melquiond |
| 2016-04-29 | Fix incorrect cbv reduction of primitive projections. (Bug #4634) | Guillaume Melquiond |
| 2016-04-28 | Make the language grammar much more precise. (Fix bugs #4682 and #4683) | Guillaume Melquiond |
| 2016-04-28 | Update tutorial (fix bug #4699). | Guillaume Melquiond |
| 2016-04-28 | Fix missing newline in coqchk engagement (bug #4694). | Guillaume Melquiond |
| 2016-04-28 | An example for cd139311e, showing a consequence of not converting | Hugo Herbelin |
| 2016-04-27 | Revert "A heuristic to add parentheses in the presence of rules such as" | Hugo Herbelin |
| 2016-04-27 | Revert "Not taking arguments given by name or position into account when" | Hugo Herbelin |
| 2016-04-27 | Revert "Adding a target for beautification." | Hugo Herbelin |
| 2016-04-27 | Revert "Adding a target check-beautify for testing reparsability of" | Hugo Herbelin |
| 2016-04-27 | Revert "So as to beautify to work, do not use notations in Inductive types" | Hugo Herbelin |
| 2016-04-27 | Revert "Protect the beautifier from change in the lexer state (typically by" | Hugo Herbelin |
| 2016-04-27 | Revert "Changing rule for "*" in Operator_Properties so that, iterated, it" | Hugo Herbelin |
| 2016-04-27 | Revert "In the short term, stronger invariant on the syntax of TacAssert, what" | Hugo Herbelin |
