coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Do not ask for a normalized goal to get hypotheses and conclusions.	Pierre-Marie Pédrot	2017-02-14
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Proofview.Goal primitive now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| *	Proofview: tclINDEPENDENTL	Enrico Tassi	2017-02-10
\| *	Unification constraint handling (#4763, #5149)	Matthieu Sozeau	2016-10-22
\|/
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
*	Adding variants enter_one and refine_one which assume that exactly one	Hugo Herbelin	2016-09-16
*	Proofview: extensions for backtracking eauto	Matthieu Sozeau	2016-06-16
*	Implement limited proof search and iterative deepening.	Matthieu Sozeau	2016-06-16
*	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\
\| *	Fix a typo in proofs/proofview.mli.	Cyprien Mangin	2016-06-14
\| *	Add goal range selectors.	Cyprien Mangin	2016-06-14
* \|	STM: proof block detection for bullets and { block }	Enrico Tassi	2016-06-06
\|/
*	Moving Evarutil and Proofview to engine/	Pierre-Marie Pédrot	2016-03-20