coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Revert "Revert "Improve the interpretation scope of arguments of an ltac matc...	Maxime Dénès	2016-07-04
*	Merge branch 'v8.5' into trunk	Maxime Dénès	2016-07-04
*	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
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	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