coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Remove deprecated objects in engine / interp / library	Emilio Jesus Gallego Arias	2018-05-30
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
*	Export Proofview.undefined as "unsafe" primitive.	Hugo Herbelin	2018-03-27
*	Adding informative variant of shelve_unifiable returning set of shelved evars.	Hugo Herbelin	2018-03-27
*	A comment in Proofview.with_shelf.	Hugo Herbelin	2018-03-08
*	Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe.	Hugo Herbelin	2018-03-08
*	Proof engine: using save_future_goal when relevant.	Hugo Herbelin	2018-03-08
*	Proof engine: consider the pair principal and future goals as an entity.	Hugo Herbelin	2018-03-08
*	Tweak comments to fix ocamldoc errors	mrmr1993	2018-03-05
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \|	Proofview: V82.tactic option to not normalize evars	Enrico Tassi	2018-03-04
* \|	proofview: debug API to print a goal	Enrico Tassi	2018-03-04
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
* \|	proofview: goals come with a state	Enrico Tassi	2018-02-20
\|/
*	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
*	Proofview: enter_one: add __LOC__ argument to get relevant error msg	Enrico Tassi	2018-01-31
*	Merge PR #6222: Share computation of unifiable evars	Maxime Dénès	2017-12-22
\|\
* \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\| *	Experimenting with a fine-grained cache for undefined evars in evinfos.	Pierre-Marie Pédrot	2017-11-21
\| *	Fix #6204: `refine` is exponential in the number of fresh evars that it creates.	Pierre-Marie Pédrot	2017-11-21
\|/
*	Fixing an old bug in collecting evars with cleared context.	Hugo Herbelin	2017-09-27
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
*	Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ...	Maxime Dénès	2017-07-07
\|\
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| *	In enter_one, not having exactly one goal is a fatal error of the monad.	Hugo Herbelin	2017-06-23
\|/
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot	2017-04-25
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/
*	"tclENV" is sexier, use it instead of "Env.get"	Matej Kosik	2017-04-20
*	reduce syntactic noise	Matej Kosik	2017-04-20
*	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
* \|	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Proofview: tclINDEPENDENTL	Enrico Tassi	2017-02-10
\| *	Merge remote-tracking branch 'github/pr/350' into trunk	Maxime Dénès	2017-01-09
\| \|\
\| * \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|/\| \|
\| \| *	tclDISPATCH: more informative error message	Arnaud Spiwack	2016-11-08
\| \|/ \|/\|
* \|	COMMENT: Proofview.entry	Matej Kosik	2016-10-26
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\ \
\| \| *	Unification constraint handling (#4763, #5149)	Matthieu Sozeau	2016-10-22
\| \|/
\| *	Oops, my bad, didn't expect a merge issue!	Matthieu Sozeau	2016-10-21
\| *	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-10-21
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\|