coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	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
\|/ / / /
\| \| * \|	Merge branch 'bug4450' into v8.5	Matthieu Sozeau	2016-06-14
\| \| \|\ \
\| \| * \ \	Merge branch 'bug4725' into v8.5	Matthieu Sozeau	2016-06-14
\| \| \|\ \ \
\| \| * \| \| \|	Admitted: fix #4818 return initial stmt and univs	Matthieu Sozeau	2016-06-14
* \| \| \| \| \|	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
\| \| \| * \| \| \|	Fix test-suite file, only part 2 is fixed in 8.5	Matthieu Sozeau	2016-06-13
* \| \| \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-13
\|\ \ \ \ \ \ \
\| \| \| \| * \| \| \|	Univs: fix for part #2 of bug #4816.	Matthieu Sozeau	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
\| \| \| \| \| \| *	Unbreak singleton list-like notation (-compat 8.4)	Jason Gross	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
\| \| \|_\|_\|_\|/ \| \|/\| \| \| \|
\| \| \| \| \| *	Univs/(e)auto: fix bug #4450 polymorphic exact hints	Matthieu Sozeau	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