coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
\| *	Goal selectors now use the keyword [only].	Cyprien Mangin	2016-06-30
\|/
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	LtacProf reports structured results (pr/209)	CJ Bell	2016-06-20
*	Do not evar-normalize goals when interpreting some hardwired genargs.	Pierre-Marie Pédrot	2016-06-20
*	Backporting c064fb933 from 8.5 (another regression with Ltac trace report).	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
*	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
*	par: like all: but in parallel	Enrico Tassi	2016-06-17
*	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
*	Purely refactoring and code/API cleanup.	Matthieu Sozeau	2016-06-16
*	bteauto: a Proofview.tactic for multiple goals	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
*	Typo in comment.	Hugo Herbelin	2016-06-16
*	Fixing space in an error message.	Hugo Herbelin	2016-06-16
*	Fixing printing of Register retroknowledge.	Hugo Herbelin	2016-06-16
*	Fixing Add Parametric Relation by adding printer for binders.	Hugo Herbelin	2016-06-16
*	Fixing missing substitution / printing cases of TacSelect.	Pierre-Marie Pédrot	2016-06-16
*	Fixing parsing of constr argument of ltac functions at level 8 in the	Hugo Herbelin	2016-06-16
*	A stronger invariant on the syntax of TacAssert, what allows for a	Hugo Herbelin	2016-06-16
*	Merge PR #195: Complete is_* family of term-examining tactics.	Pierre-Marie Pédrot	2016-06-16
\|\
* \	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\ \
* \ \	Merge PR #211: Fix a printing typo in LtacProf.	Pierre-Marie Pédrot	2016-06-16
\|\ \ \
* \ \ \	Merge PR #100: fresh now accepts more things than just identifiers.	Pierre-Marie Pédrot	2016-06-16
\|\ \ \ \
\| \| \| \| *	Add is_const	Jason Gross	2016-06-16
\| \| * \| \|	Fix another missing newline	Jason Gross	2016-06-16
\| \| * \| \|	Fix a printing typo	Jason Gross	2016-06-16
\| \|/ / / \|/\| \| \|
* \| \| \|	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
\| \| \| * \|	Fix usage of Pervasives in goal selectors.	Cyprien Mangin	2016-06-14
\| \| \| * \|	Fix the pretty-printing of goal range 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
\| * \| \| \|	Revert "Strip some trailing spaces"	Pierre-Marie Pédrot	2016-06-13
* \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-09
\| \| \| \| *	Add is_ind, is_constructor, is_proj	Jason Gross	2016-06-07
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	About printing of traces of failures while calling ltac code.	Hugo Herbelin	2016-06-06
\| \| * \|	STM: proof block detection for par:	Enrico Tassi	2016-06-06
\| \| * \|	STM: proof block detection/error resilience API	Enrico Tassi	2016-06-06
\| \|/ / \|/\| \|