coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-09
\|\
* \|	printing.mllib: remove some other .mli-only from a .mllib	Pierre Letouzey	2016-06-07
\| *	Fixing problems introduced in 8.5 with Ltac trace report. E.g.	Hugo Herbelin	2016-06-06
* \|	About printing of traces of failures while calling ltac code.	Hugo Herbelin	2016-06-06
* \|	Removing "rename" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
* \|	Removing "exact" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
* \|	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
* \|	Removing "double induction" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
* \|	Move ide serialization libraries from lib/ to ide/	Emilio Jesus Gallego Arias	2016-06-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\\|
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\| *	Pfedit.get_current_context refinement (fix #4523)	Matthieu Sozeau	2016-05-26
* \|	Put the "cofix" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \|	Put the "fix" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \|	Put the "clear" tactic into the monad.	Pierre-Marie Pédrot	2016-05-16
* \|	Actually using the symbol information to print Tactic Notations properly.	Pierre-Marie Pédrot	2016-05-08
* \|	Removing dead code in Pptactic.	Pierre-Marie Pédrot	2016-05-08
* \|	Pass user symbol to tactic notation printers.	Pierre-Marie Pédrot	2016-05-08
* \|	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
* \|	Normalizing the names of dynamic types to follow a typ_* scheme.	Pierre-Marie Pédrot	2016-05-04
* \|	Removing useless generic arguments.	Pierre-Marie Pédrot	2016-05-04
* \|	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
* \|	Switching to an untyped toplevel representation for Ltac values.	Pierre-Marie Pédrot	2016-05-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\|
\| *	Remove extraneous space in coqtop/pg output (bug #4675).	Guillaume Melquiond	2016-05-03
* \|	Revert "A heuristic to add parentheses in the presence of rules such as"	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 "In the short term, stronger invariant on the syntax of TacAssert, what"	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 "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 "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
* \|	Revert "Fixing printing of Register retroknowledge."	Hugo Herbelin	2016-04-27
* \|	Revert "Passing around the precedence to the generic printer so as to solve"	Hugo Herbelin	2016-04-27