coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge remote-tracking branch 'github/pr/229' into trunk	Maxime Dénès	2016-07-04
\|\
* \|	Revert "Revert "Improve the interpretation scope of arguments of an ltac matc...	Maxime Dénès	2016-07-04
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2016-07-04
\|\ \
* \| \|	Update CHANGES, the bugfixes for 4527 and 4726 are	Matthieu Sozeau	2016-07-04
\| * \|	Mention more fixes in CHANGES before we release pl2.	Maxime Dénès	2016-07-04
\| * \|	Revert "Improve the interpretation scope of arguments of an ltac match."	Maxime Dénès	2016-07-04
\| * \|	test-suite: test checking of libraries checksum.	Maxime Dénès	2016-07-04
\| * \|	Merge remote-tracking branch 'github/pr/228' into v8.5	Maxime Dénès	2016-07-04
\| \|\ \
* \| \| \|	Remove lexing of ordinal notations.	Maxime Dénès	2016-07-03
* \| \| \|	Mention recent renaming of files in dev/doc/changes.txt.	Maxime Dénès	2016-07-03
* \| \| \|	Merge branch 'cerrors-cclosure' into trunk	Maxime Dénès	2016-07-03
\|\ \ \ \
\| * \| \| \|	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
* \| \| \| \|	Adding test for #4811.	Hugo Herbelin	2016-07-02
\|/ / / /
* \| \| \|	Merge branch 'reduction-flags' into trunk	Maxime Dénès	2016-07-01
\|\ \ \ \
\| * \| \| \|	Add and document match, fix and cofix reduction flags.	Maxime Dénès	2016-07-01
\| * \| \| \|	Make semantics of whd_zeta consistent with other whd_* functions.	Maxime Dénès	2016-07-01
\| \| * \| \|	Fixing use of "Declare Implicit Tactic" in refine.	Hugo Herbelin	2016-07-01
\| * \| \| \|	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
\|/ / / /
\| * \| \|	Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack).	Hugo Herbelin	2016-07-01
\| * \| \|	Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).	Hugo Herbelin	2016-07-01
\| \| \| *	Makefile: $(BEST) controls which coqtop is used to build .vo	Pierre Letouzey	2016-06-29
\| \| \| *	coq_makefile : do not build bytecode versions of plugins by default	Pierre Letouzey	2016-06-29
\| \| \| *	Makefile: no bytecode compilation in make world, see make byte instead	Pierre Letouzey	2016-06-29
\| \|_\|/ \|/\| \|
* \| \|	Fixing #4865 (deciding on which arguments to recompute scopes was not robust).	Hugo Herbelin	2016-06-29
* \| \|	Exporting section_segment_of_reference.	Hugo Herbelin	2016-06-29
* \| \|	Updated CHANGES about subst. More on recursive equations in reference manual.	Hugo Herbelin	2016-06-29
* \| \|	Merge branch 'programcases' into trunk	Matthieu Sozeau	2016-06-29
\|\ \ \
\| * \| \|	Fixes in documentation.	Matthieu Sozeau	2016-06-29
\| * \| \|	Program: cleanup in cases, add options	Matthieu Sozeau	2016-06-29
\|/ / /
* \| \|	Merge branch 'bug4527' into trunk	Matthieu Sozeau	2016-06-29
\|\ \ \
\| * \| \|	Univ: Use loc even if there are more unbound levels	Matthieu Sozeau	2016-06-29
\| * \| \|	CHANGES: document fix for #4726 too.	Matthieu Sozeau	2016-06-29
\| * \| \|	CHANGES: document fix for 4527 and compatibility.	Matthieu Sozeau	2016-06-29
\| * \| \|	universes.ml: Minor code cleanup	Matthieu Sozeau	2016-06-29
\| * \| \|	Univs: Fix bug #4726	Matthieu Sozeau	2016-06-29
\| * \| \|	Univs: add source locations of levels	Matthieu Sozeau	2016-06-29
\| * \| \|	Univs: earlier errors for strict univ decls #4527	Matthieu Sozeau	2016-06-29
\|/ / /
* \| \|	Merge branch 'warnings' into trunk	Maxime Dénès	2016-06-29
\|\ \ \
\| * \| \|	Fix issues in test-suite revealed by warnings.	Maxime Dénès	2016-06-29
\| * \| \|	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
\| * \| \|	Add [Unset Printing Dependent Evars Line]	Jason Gross	2016-06-29
\| \| \| *	fix coqide double module linking (error on OCaml 4.03)	Gabriel Scherer	2016-06-28
\| \| \|/
* \| \|	Revert "A new infrastructure for warnings."	Maxime Dénès	2016-06-28
* \| \|	Typeclasses: use once in by clause for typeclass eauto	Matthieu Sozeau	2016-06-28
* \| \|	Merge branch 'warnings' into trunk	Maxime Dénès	2016-06-28
\|\ \ \
\| * \| \|	A new infrastructure for warnings.	Maxime Dénès	2016-06-28
\|/ / /
* \| \|	Merge remote-tracking branch 'github/pr/207' into trunk	Maxime Dénès	2016-06-28
\|\ \ \ \| \|/ / \|/\| \|
\| \| *	Merge branch 'forhott' into v8.5	Matthieu Sozeau	2016-06-28
\| \| \|\