coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Test-suite fix to 1744e37 (injection in context).	Hugo Herbelin	2016-06-18
*	Adding an "as" clause to specialize.	Hugo Herbelin	2016-06-18
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin	2016-06-18
*	par: like all: but in parallel	Enrico Tassi	2016-06-17
*	proof mode: print unification constraints	Matthieu Sozeau	2016-06-16
*	Tentative fix of test-suite file to avoid loop	Matthieu Sozeau	2016-06-16
*	Cleanup and refactoring	Matthieu Sozeau	2016-06-16
*	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
*	Example given at DeepSpec workshop	Matthieu Sozeau	2016-06-16
*	Purely refactoring and code/API cleanup.	Matthieu Sozeau	2016-06-16
*	eauto: fix test-suite file	Matthieu Sozeau	2016-06-16
*	bteauto: a Proofview.tactic for multiple goals	Matthieu Sozeau	2016-06-16
*	Fix iterative deepening strategy failing too early	Matthieu Sozeau	2016-06-16
*	Implement limited proof search and iterative deepening.	Matthieu Sozeau	2016-06-16
*	Typeclasses eauto based on new proof engine,	Matthieu Sozeau	2016-06-16
*	Refine 9cc95f5, unification of Let-In's, bug #3929	Matthieu Sozeau	2016-06-16
*	Not taking arguments given by name or position into account when	Hugo Herbelin	2016-06-16
*	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\
* \	Merge branch 'pr/146' into trunk	Enrico Tassi	2016-06-16
\|\ \
* \| \|	Fix test-suite for opened bug #4813.	Pierre-Marie Pédrot	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
* \| \|	fix test-suite/ide Makefile (stupid typo)	Enrico Tassi	2016-06-15
\|/ /
* \|	test-suiet: run fake_id as before pr/173 was merged	Enrico Tassi	2016-06-14
* \|	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\ \
\| \| *	Ident selectors cannot be used inside an Ltac expression.	Cyprien Mangin	2016-06-14
\| \| *	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin	2016-06-14
\| \| *	Remove the need for brackets in goal selectors.	Cyprien Mangin	2016-06-14
\| \| *	Add test-suite file for goal selectors.	Cyprien Mangin	2016-06-14
\| \|/ \|/\|
* \|	Merge branch "LtacProf for trunk" (PR #165).	Pierre-Marie Pédrot	2016-06-14
\|\ \
* \| \|	Univs: more robust Universe/Constraint decls #4816	Matthieu Sozeau	2016-06-13
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-13
\|\ \ \
* \| \| \|	For the record, an example one would like to see working.	Hugo Herbelin	2016-06-12
\| * \| \|	Another fix to #4782 (a typing error not captured when dealing with bindings).	Hugo Herbelin	2016-06-12
\| * \| \|	Fixing #4782 (a typing error not captured when dealing with bindings).	Hugo Herbelin	2016-06-11
* \| \| \|	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
* \| \| \|	Test for #4787.	Hugo Herbelin	2016-06-07
\| \| \| *	Error box detection run only on error	Enrico Tassi	2016-06-06
\| \| \| *	STM: proof block detection made optional + simple test	Enrico Tassi	2016-06-06
* \| \| \|	About printing of traces of failures while calling ltac code.	Hugo Herbelin	2016-06-06
\| \|_\|/ \|/\| \|
\| \| *	Improve a comment in the test suite	Jason Gross	2016-06-05
\| \| *	Make Ltac Profiling an setting	Jason Gross	2016-06-05
\| \| *	LtacProf for Coq trunk	Jason Gross	2016-06-05
\| \|/ \|/\|
* \|	Removing "exact" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
* \|	Update primitive coinductive test-suite.	Matthieu Sozeau	2016-06-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\\|
\| *	Fix bug #4746: Anomaly: Evar ?X10 was not declared.	Pierre-Marie Pédrot	2016-05-29
\| *	rewrite/Univs: Fix bug # 4498.	Matthieu Sozeau	2016-05-26