coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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 parsing of constr argument of ltac functions at level 8 in the	Hugo Herbelin	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
*	In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.	Hugo Herbelin	2016-06-16
*	Adding option "Set Reversible Pattern Implicit" to Specif.v so that an	Hugo Herbelin	2016-06-16
*	Being defensive in printing implicit arguments also with manual	Hugo Herbelin	2016-06-16
*	A stronger invariant on the syntax of TacAssert, what allows for a	Hugo Herbelin	2016-06-16
*	Changing rule for "*" in Operator_Properties so that, iterated, it	Hugo Herbelin	2016-06-16
*	Protect the beautifier from change in the lexer state (typically by	Hugo Herbelin	2016-06-16
*	Not taking arguments given by name or position into account when	Hugo Herbelin	2016-06-16
*	Merge '/pr/206' into trunk	Enrico Tassi	2016-06-16
\|\
* \	Merge PR #195: Complete is_* family of term-examining tactics.	Pierre-Marie Pédrot	2016-06-16
\|\ \
* \ \	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\ \ \
* \ \ \	Merge PR #211: Fix a printing typo in LtacProf.	Pierre-Marie Pédrot	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 PR #100: fresh now accepts more things than just identifiers.	Pierre-Marie Pédrot	2016-06-16
\|\ \ \ \ \ \
* \| \| \| \| \| \|	Fix Makefile after ssrmatching merge	Enrico Tassi	2016-06-16
* \| \| \| \| \| \|	--print-version produces machine readable version info	Enrico Tassi	2016-06-16
* \| \| \| \| \| \|	ideslave: do not bail out in case of XML error	Enrico Tassi	2016-06-16
* \| \| \| \| \| \|	Remove inappropriate comment.	Maxime Dénès	2016-06-16
\| \| \| \| \| * \|	Update CHANGES	Jason Gross	2016-06-16
\| \| \| \| \| * \|	Add is_const	Jason Gross	2016-06-16
* \| \| \| \| \| \|	Merge branch 'pr/146' into trunk	Enrico Tassi	2016-06-16
\|\ \ \ \ \ \ \
\| * \| \| \| \| \| \|	Ignore generated .ml file for ssrmatching	Enrico Tassi	2016-06-16
* \| \| \| \| \| \| \|	Merge remote-tracking branch 'github/pr/194' into trunk	Maxime Dénès	2016-06-16
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	Fix another missing newline	Jason Gross	2016-06-16
\| \| \| \| \| * \| \| \|	Fix a printing typo	Jason Gross	2016-06-16
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	Fixing the checker.	Pierre-Marie Pédrot	2016-06-16
\| \| \| \| * \| \| \|	Remove the syntax changes introduced by this branch.	Pierre-Marie Pédrot	2016-06-15
* \| \| \| \| \| \| \|	Fix test-suite for opened bug #4813.	Pierre-Marie Pédrot	2016-06-15
\| \| \| \| * \| \| \|	Allow `Pretyping.search_guard` to not check guard	Arnaud Spiwack	2016-06-15
\| \| * \| \| \| \| \|	ssrmatching: giving proper credits to the original author(s)	Enrico Tassi	2016-06-15
\| \| * \| \| \| \| \|	Merge branch 'pr/146' into trunk	Enrico Tassi	2016-06-15
\| \|/\| \| \| \| \| \| \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	ssrmatching: simple test for Ltac API	Enrico Tassi	2016-06-15
\| \| * \| \| \| \| \|	ssrmatching: ltac argument parsing made more robust	Enrico Tassi	2016-06-15
\| \| * \| \| \| \| \|	ssrmatching: debug prints sent via msg_debug	Enrico Tassi	2016-06-15
\| \| * \| \| \| \| \|	Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"	Enrico Tassi	2016-06-15
* \| \| \| \| \| \| \|	typography	Matej Kosik	2016-06-15
* \| \| \| \| \| \| \|	ocamllibdep + coqdep : simpler deps concerning .mllib and .mlpack	Pierre Letouzey	2016-06-15
* \| \| \| \| \| \| \|	Makefile.build: ensure a build failure in case of a missing rule	Pierre Letouzey	2016-06-15
* \| \| \| \| \| \| \|	fix test-suite/ide Makefile (stupid typo)	Enrico Tassi	2016-06-15
\| \| \| \| * \| \| \|	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14