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
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-12	[tactics] Remove dependency of abstract on global proof state.	Emilio Jesus Gallego Arias
2019-01-31	[proof] optimize proof always works on incomplete proofs	Enrico Tassi
2018-12-13	[engine] Allow debug printers to access the environment.	Emilio Jesus Gallego Arias
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-10-26	[typeclasses] functionalize typeclass evar handling	Matthieu Sozeau
2018-10-26	Cleanup evar_extra: remove evar_info's store and add maps to evar_map	Matthieu Sozeau
2018-07-17	Change QuestionMark for better record field missing error message.	Siddharth Bhat
2018-06-04	[econstr] Remove some Unsafe.to_constr use.	Emilio Jesus Gallego Arias
2018-05-30	[api] Remove deprecated objects in engine / interp / library	Emilio Jesus Gallego Arias
2018-04-13	Evar maps contain econstrs.	Gaëtan Gilbert
2018-03-27	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-08	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-05	Tweak comments to fix ocamldoc errors	mrmr1993
2018-03-05	Merge PR #6855: Update headers following #6543.	Maxime Dénès
2018-03-04	Proofview: V82.tactic option to not normalize evars	Enrico Tassi
2018-03-04	proofview: debug API to print a goal	Enrico Tassi
2018-02-27	Update headers following #6543.	Théo Zimmermann
2018-02-20	proofview: goals come with a state	Enrico Tassi
2018-02-12	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias
2018-01-31	Proofview: enter_one: add __LOC__ argument to get relevant error msg	Enrico Tassi
2017-12-22	Merge PR #6222: Share computation of unifiable evars	Maxime Dénès
2017-11-22	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias
2017-11-21	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-09-27	Fixing an old bug in collecting evars with cleared context.	Hugo Herbelin
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík
2017-07-07	Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ...	Maxime Dénès
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-23	In enter_one, not having exactly one goal is a fatal error of the monad.	Hugo Herbelin
2017-06-06	Remove the Sigma (monotonous state) API.	Maxime Dénès
2017-05-30	Support for using type information to infer more precise evar sources.	Hugo Herbelin
2017-05-27	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias
2017-05-24	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias
2017-04-25	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot
2017-04-25	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias
2017-04-20	"tclENV" is sexier, use it instead of "Env.get"	Matej Kosik
2017-04-20	reduce syntactic noise	Matej Kosik
2017-02-14	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