coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Fixing missing parentheses in printing of patterns in binders.	Hugo Herbelin	2016-07-19
* \|	primproj: warning and avoid error.	Matthieu Sozeau	2016-07-06
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	Add and document match, fix and cofix reduction flags.	Maxime Dénès	2016-07-01
* \|	Merge remote-tracking branch 'github/pr/207' into trunk	Maxime Dénès	2016-06-28
\|\ \
* \| \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
\| * \|	Add [Unset Printing Dependent Evars Line]	Jason Gross	2016-06-19
\|/ /
* \|	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
* \|	Print the type-in-type flag in various user-facing functions.	Pierre-Marie Pédrot	2016-06-18
* \|	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin	2016-06-18
* \|	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
* \|	proof mode: print unification constraints	Matthieu Sozeau	2016-06-16
* \|	Extend Hint Mode to handle the no-head-evar case	Matthieu Sozeau	2016-06-16
* \|	Isolating and exporting a function for printing body of a recursive definition.	Hugo Herbelin	2016-06-16
* \|	Simplification in ppvernac.ml.	Hugo Herbelin	2016-06-16
* \|	Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.	Hugo Herbelin	2016-06-16
* \|	Fixing extra space in printing bullets.	Hugo Herbelin	2016-06-16
* \|	Fixing space in printing <+ and <: + fixing missing Inline keyword.	Hugo Herbelin	2016-06-16
* \|	Fixing printing of Instance.	Hugo Herbelin	2016-06-16
* \|	Fixing extra space in printing abbreviations (SyntaxDefinition).	Hugo Herbelin	2016-06-16
* \|	Fixing printing of Polymorphic/Monomorphic.	Hugo Herbelin	2016-06-16
* \|	Fixing printing of Arguments.	Hugo Herbelin	2016-06-16
* \|	Printing notations as parsed.	Hugo Herbelin	2016-06-16
* \|	So as to beautify to work, do not use notations in Inductive types	Hugo Herbelin	2016-06-16
* \|	Fixing missing substitution / printing cases of TacSelect.	Pierre-Marie Pédrot	2016-06-16
* \|	Fixing printing of keeping hyp on the fly.	Hugo Herbelin	2016-06-16
* \|	Fixing printing of inversion as.	Hugo Herbelin	2016-06-16
* \|	Fixing extra space in printing destruct/induction as.	Hugo Herbelin	2016-06-16
* \|	Fixing printing of induction/destruct as.	Hugo Herbelin	2016-06-16
* \|	Fixing printing of pat%constr.	Hugo Herbelin	2016-06-16
* \|	A stronger invariant on the syntax of TacAssert, what allows for a	Hugo Herbelin	2016-06-16
* \|	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\ \
* \ \	Merge remote-tracking branch 'github/pr/194' into trunk	Maxime Dénès	2016-06-16
\|\ \ \
\| \| * \|	Remove the syntax changes introduced by this branch.	Pierre-Marie Pédrot	2016-06-15
\| \| * \|	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \| \| \|	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
\| \| * \|	Adding an only printing flag to notations.	Pierre-Marie Pédrot	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