coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove the need for brackets in goal selectors.	Cyprien Mangin	2016-06-14
*	Fix a typo in proofs/proofview.mli.	Cyprien Mangin	2016-06-14
*	Fix usage of Pervasives in goal selectors.	Cyprien Mangin	2016-06-14
*	Add a comment about the use of a zipper, for clarity.	Cyprien Mangin	2016-06-14
*	Fix the pretty-printing of goal range selectors.	Cyprien Mangin	2016-06-14
*	Add a [CList.partitioni] function.	Cyprien Mangin	2016-06-14
*	Add test-suite file for goal selectors.	Cyprien Mangin	2016-06-14
*	Add goal range selectors.	Cyprien Mangin	2016-06-14
*	Merge branch "LtacProf for trunk" (PR #165).	Pierre-Marie Pédrot	2016-06-14
\|\
\| *	Commenting out debugging code.	Pierre-Marie Pédrot	2016-06-14
\| *	Correct use of printing primitives.	Pierre-Marie Pédrot	2016-06-14
\| *	Better coding style (semantics).	Pierre-Marie Pédrot	2016-06-14
\| *	Better coding style (syntax).	Pierre-Marie Pédrot	2016-06-14
\| *	Adding Coq headers.	Pierre-Marie Pédrot	2016-06-14
\| *	Moving back Ltac profiling to the Ltac folder.	Pierre-Marie Pédrot	2016-06-14
* \|	Merge remote-tracking branch 'github/evarunsafe' into trunk	Matthieu Sozeau	2016-06-14
\|\ \
\| \| *	Moving UTF-8 related functions to Unicode module.	Pierre-Marie Pédrot	2016-06-14
\| \| *	Revert "Strip some trailing spaces"	Pierre-Marie Pédrot	2016-06-13
* \| \|	Univs: more robust Universe/Constraint decls #4816	Matthieu Sozeau	2016-06-13
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-13
\|\ \ \
\| * \| \|	evar_conv: Refine occur_rigidly	Matthieu Sozeau	2016-06-13
\| * \| \|	Tentatively fixing misguiding error message with "binder" type in	Hugo Herbelin	2016-06-13
* \| \| \|	For the record, an example one would like to see working.	Hugo Herbelin	2016-06-12
\| * \| \|	Minor simplification in evarconv.	Hugo Herbelin	2016-06-12
\| * \| \|	Another fix to #4782 (a typing error not captured when dealing with bindings).	Hugo Herbelin	2016-06-12
\| * \| \|	Reserve exception "ConversionFailed" in unification for failure of	Hugo Herbelin	2016-06-12
\| * \| \|	Protecting eta-expansion in evarconv.ml against ill-typed problems.	Hugo Herbelin	2016-06-12
\| * \| \|	Fixing bug in printing CannotSolveConstraint (collision of context names).	Hugo Herbelin	2016-06-12
\| * \| \|	Fixing #4782 (a typing error not captured when dealing with bindings).	Hugo Herbelin	2016-06-11
\| * \| \|	Fixing a try with in apply that has become too weak in 8.5.	Hugo Herbelin	2016-06-11
* \| \| \|	Merge branch 'pack-plugins'	Pierre Letouzey	2016-06-10
\|\ \ \ \
* \| \| \| \|	coq_makefile: oups, a missing ; in my previous commit	Pierre Letouzey	2016-06-10
\| * \| \| \|	coq_makefile: fix a crucial typo in e9c57a3	Pierre Letouzey	2016-06-10
* \| \| \| \|	coq_makefile: short display of COQC and COQDEP (follow-up of e9c57a3)	Pierre Letouzey	2016-06-10
* \| \| \| \|	A mini-optimization for free in unification.ml: test in O(1)	Hugo Herbelin	2016-06-10
\| \| * \| \|	Reporting about a few bug fixes (to be continued).	Hugo Herbelin	2016-06-09
\| \| \| * \|	newring: fix for hack using evars as integers.	Matthieu Sozeau	2016-06-09
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot	2016-06-09
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-09
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Fixing #4644 (regression of unification on evar-evar problems with a match).	Hugo Herbelin	2016-06-09
\| * \| \|	Minor simplification in evarconv.ml.	Hugo Herbelin	2016-06-09
\| * \| \|	New update on how to find camlp5 binary and library at configure time.	Hugo Herbelin	2016-06-09
\| * \| \|	Improve the interpretation scope of arguments of an ltac match.	Hugo Herbelin	2016-06-09
\| * \| \|	Reverting dbdff037 which does not seem to prevent to have #3638 fixed	Hugo Herbelin	2016-06-09
* \| \| \|	Documenting API changes in dev/doc/changes.txt.	Pierre-Marie Pédrot	2016-06-09
* \| \| \|	Merge PR #190: Add configurable shortcuts for user queries to CoqIDE.	Pierre-Marie Pédrot	2016-06-09
\|\ \ \ \
* \ \ \ \	Merge PR #197.	Pierre-Marie Pédrot	2016-06-09
\|\ \ \ \ \
\| \| \| * \| \|	Remove failure on non-.v files (bug #4752).	Guillaume Melquiond	2016-06-09
* \| \| \| \| \|	Adding profiling developer information in dev/doc/profiling.txt.	Pierre-Marie Pédrot	2016-06-08
\| * \| \| \| \|	Add an explicit replacement rule for Refine module	Jason Gross	2016-06-08
\|/ / / / /