coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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-04
\| \| * \|	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-03
\| \| * \|	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-05-02
\| * \| \|	Reduce ide/coq.png to 256x256.	Guillaume Melquiond	2016-04-29
\| * \| \|	Fix incorrect cbv reduction of primitive projections. (Bug #4634)	Guillaume Melquiond	2016-04-29
\| * \| \|	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-28
* \| \| \|	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	2016-04-27
* \| \| \|	Revert "Being defensive in printing implicit arguments also with manual"	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Temporary deactivate re-interpretation of terms in beautify."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ...	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing printers for pr_auto_using and pr_firstorder_using."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing printing of pat%constr."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing printing of induction/destruct as."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing extra space in printing destruct/induction as."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing printing of inversion as."	Hugo Herbelin	2016-04-27