coq - The formal proof system

Age	Commit message (Expand)	Author
2019-03-25	Fix #9652: rewrite fails to detect lack of progress	Gaëtan Gilbert
2018-10-30	Avoid passing dummy env to error printer	Maxime Dénès
2018-10-26	Cleanup evar_extra: remove evar_info's store and add maps to evar_map	Matthieu Sozeau
2018-09-17	Ensure_prev_proof returns a proof that has underlying differences from	Jim Fehrle
2018-03-27	Congruence: getting rid of a detour by the compatibility layer of proof engine.	Hugo Herbelin
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-11-29	[proof] [api] Rename proof types in preparation for functionalization.	Emilio Jesus Gallego Arias
2017-11-04	Finish removing Show Goal uid	Gaëtan Gilbert
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-04-24	Removing the tclWEAK_PROGRESS tactical.	Pierre-Marie Pédrot
2017-02-14	Funind API using EConstr.	Pierre-Marie Pédrot
2017-02-14	Goal API using EConstr.	Pierre-Marie Pédrot
2016-06-09	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-11	CLEANUP: kernel/context.ml{,i}	Matej Kosik
2015-01-12	Update headers.	Maxime Dénès
2014-10-16	Goal: remove [advance] from the API.	Arnaud Spiwack
2014-10-16	Goal: remove some functions from the compatibility layer.	Arnaud Spiwack
2014-10-16	Goal: remove most of the API (make [Goal.goal] concrete).	Arnaud Spiwack
2014-10-16	Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...	Arnaud Spiwack
2014-10-13	Adding a tactic which fails if one of the goals under focus is dependent in a...	Hugo Herbelin
2014-09-30	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin
2014-09-27	Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.	Pierre-Marie Pédrot
2014-09-12	Use evar name to print goal.	Hugo Herbelin
2014-09-04	Ensuring the invariant that hypotheses and named context of the environment of	Pierre-Marie Pédrot
2014-09-03	Putting back normalized goals when entering them.	Pierre-Marie Pédrot
2014-08-21	Removing unused parts of the Goal.sensitive monad.	Pierre-Marie Pédrot
2014-08-19	Removing a use of Goal.refine.	Pierre-Marie Pédrot
2014-08-05	Goal: API to get the solution of a goal	Enrico Tassi
2014-02-27	Code refactoring thanks to the new Monad module.	Arnaud Spiwack
2014-01-10	Exporting the full pretyper options in Goal.constr_of_raw.	Pierre-Marie Pédrot
2013-11-30	Fixing ltac constr variable handling in refine.	Pierre-Marie Pédrot
2013-11-02	Add primitives in Goal.V82 to access the goal in nf_evar'd form.	aspiwack
2013-11-02	A tactic shelve_unifiable.	aspiwack
2013-11-02	Tachmach.New is now in Proofview.Goal.enter style.	aspiwack
2013-11-02	Try to remove intermediate allocations when dealing with goal-specific tactics.	aspiwack
2013-11-02	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-10-05	Moving side effects into evar_map. There was no reason to keep another	ppedrot
2013-08-25	Replacing lists by sets in clear tactic.	ppedrot
2013-08-08	State Transaction Machine	gareuselesinge
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-12	Allowing different types of, not to be mixed, generic Stores through	ppedrot
2013-01-29	No reason a priori for using unfiltered env for printing	herbelin
2013-01-29	Fixed synchronicity of filter with evar context in new_goal_with.	herbelin
2012-12-14	Modulification of identifier	ppedrot
2012-08-08	Updating headers.	herbelin