coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \|	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
* \| \| \|	Revert "Fixing printing of keeping hyp on the fly."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Protect printing of intro-patterns from collision when "[\|" or "\|]""	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Protect printing of ltac's "context [...]" from possible collision"	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Revert "Protect printing of intro-patterns from collision when "[\|" or"	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Printing notations as parsed."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing printing of Arguments."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing printing of Polymorphic/Monomorphic."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing printing of Instance."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Fixing extra space in printing bullets."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Removing unused generalization of pr_vernac over pr_constr and pr_lco...	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Simplification in ppvernac.ml."	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Isolating and exporting a function for printing body of a recursive d...	Hugo Herbelin	2016-04-27