coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \| \| \|	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
\| \| \|\ \
* \| \| \ \	Finalizing the only printing feature.	Pierre-Marie Pédrot	2016-06-28
\|\ \ \ \ \
\| * \| \| \| \|	Documenting the "only printing" notation flag.	Pierre-Marie Pédrot	2016-06-28
\| * \| \| \| \|	Adding a test-suite for the only printing flag.	Pierre-Marie Pédrot	2016-06-28
\| * \| \| \| \|	Properly handle the only printing flag in Reserved Notations.	Pierre-Marie Pédrot	2016-06-28