coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Revert "Merge remote-tracking branch 'github/pr/229' into trunk"	Maxime Dénès	2016-07-05
*	Merge remote-tracking branch 'github/pr/229' into trunk	Maxime Dénès	2016-07-04
\|\
* \|	rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...	Pierre Letouzey	2016-07-03
* \|	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
* \|	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
* \|	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
\| *	Makefile: no bytecode compilation in make world, see make byte instead	Pierre Letouzey	2016-06-29
\|/
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-27
\|\
* \|	ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTEND	Pierre Letouzey	2016-06-27
* \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
* \|	Removing tactic compatibility layers in setoid_ring.	Pierre-Marie Pédrot	2016-06-24
\| *	Fix typo.	Guillaume Melquiond	2016-06-23
* \|	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot	2016-06-18
* \|	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
* \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
* \|	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
* \|	Factorizing the uses of Declareops.safe_flags.	Pierre-Marie Pédrot	2016-06-16
* \|	Fixing a mispelling coma -> comma.	Hugo Herbelin	2016-06-16
* \|	Adding printers for ring and field commands.	Hugo Herbelin	2016-06-16
* \|	Fixing printing of Function.	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
\|\ \
* \| \|	Remove inappropriate comment.	Maxime Dénès	2016-06-16
\| * \|	Remove the syntax changes introduced by this branch.	Pierre-Marie Pédrot	2016-06-15
* \| \|	ssrmatching: giving proper credits to the original author(s)	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
\| * \|	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \| \|	port ssrmatching plugin to the new makefile	Enrico Tassi	2016-06-14
* \| \|	Merge remote-tracking branch 'origin/pr/146' into trunk	Enrico Tassi	2016-06-14
\|\ \ \
\| \| \| *	Merge branch 'bug4725' into v8.5	Matthieu Sozeau	2016-06-14
\| \| \| \|\
* \| \| \| \	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\ \ \ \ \
* \ \ \ \ \	Merge remote-tracking branch 'github/evarunsafe' into trunk	Matthieu Sozeau	2016-06-14
\|\ \ \ \ \ \
\| * \| \| \| \| \|	newring: fix for hack using evars as integers.	Matthieu Sozeau	2016-06-09
* \| \| \| \| \| \|	Compilation via pack for plugins of the stdlib	Pierre Letouzey	2016-06-08
\|/ / / / / /
* \| \| \| \| \|	Officially discontinue the experimental coq build via ocamlbuild	Pierre Letouzey	2016-06-08
\| * \| \| \| \|	STM: proof block detection/error resilience API	Enrico Tassi	2016-06-06
\|/ / / / /
* \| \| \| \|	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
* \| \| \| \|	A slight phase of documentation and uniformization of names of	Hugo Herbelin	2016-06-02
* \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\ \ \ \ \ \| \| \|_\|/ / \| \|/\| \| \|
* \| \| \| \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\| * \| \| \|	Extraction : add a location in the error message about polyprop	Pierre Letouzey	2016-05-30
* \| \| \| \|	Extraction : add a location in the error message about polyprop	Pierre Letouzey	2016-05-30
\| \| \| \| *	Univs/Program/Function: Fix bug #4725	Matthieu Sozeau	2016-05-26
\| \| \|_\|/ \| \|/\| \|
\| * \| \|	Extraction/Projections: Fix bug #4710	Matthieu Sozeau	2016-05-23
\| * \| \|	Disable memoization rather than failing when files cannot be opened.	Guillaume Melquiond	2016-05-20
* \| \| \|	Extraction: code cleanup in Common	Pierre Letouzey	2016-05-20
\| * \| \|	Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19