coq - The formal proof system

Age	Commit message (Expand)	Author
2019-05-14	Allow run_tactic to return a value, remove hack from ltac2	Gaëtan Gilbert
2019-05-10	[api] Remove 8.10 deprecations.	Emilio Jesus Gallego Arias
2019-04-05	[api] [proofs] Remove dependency of proofs on interp.	Emilio Jesus Gallego Arias
2019-01-21	At Qed, if shelved goals remain, emit a warning instead of an error	Maxime Dénès
2018-12-14	[proof] Rework proof interface.	Emilio Jesus Gallego Arias
2018-11-19	[proof] Provide better control of "open proofs" exceptions.	Emilio Jesus Gallego Arias
2018-10-06	[api] Remove (most) 8.9 deprecated objects.	Emilio Jesus Gallego Arias
2018-09-17	Ensure_prev_proof returns a proof that has underlying differences from	Jim Fehrle
2018-08-27	Add support for focusing on named goals using brackets.	Théo Zimmermann
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-26	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias
2017-11-19	[proof] Attempt to deprecate some V82 parts of the proof API.	Emilio Jesus Gallego Arias
2017-11-13	[api] Insert miscellaneous API deprecation back to core.	Emilio Jesus Gallego Arias
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-02-14	Merge branch 'master'.	Pierre-Marie Pédrot
2017-02-14	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot
2017-01-26	Adding a printer for Proof.proof reflecting the focusing layout.	Hugo Herbelin
2016-01-20	Update copyright headers.	Maxime Dénès
2015-09-20	Proof: suggest Admitted->Qed only if the proof is really complete (#4349)	Enrico Tassi
2015-05-29	STM/Univ: save initial univs (the ones in the statement) in Proof.proof	Enrico Tassi
2015-02-23	Fix some typos in comments.	Guillaume Melquiond
2015-01-12	Update headers.	Maxime Dénès
2014-11-09	new: Optimize Proof, Optimize Heap	Enrico Tassi
2014-11-01	Add [Info] command.	Arnaud Spiwack
2014-10-22	Remove unused functions for side effects.	Arnaud Spiwack
2014-10-01	Factored out IDE goal structure.	Carst Tankink
2014-07-31	Making the error message about bullets more precise.	Pierre Courtieu
2014-07-23	Proof_global.start_dependent_proof: properly threads the sigma through the te...	Arnaud Spiwack
2014-06-18	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-12-04	Allow proofs to start with dependent goals.	Arnaud Spiwack
2013-11-04	Allowing proofs starting with a non-empty evarmap.	ppedrot
2013-11-02	Update comments.	aspiwack
2013-11-02	Adds a tactic give_up.	aspiwack
2013-11-02	Adds a shelve tactic.	aspiwack
2013-11-02	The tactic [admit] exits with the "unsafe" status.	aspiwack
2013-10-05	Moving side effects into evar_map. There was no reason to keep another	ppedrot
2013-08-08	State Transaction Machine	gareuselesinge
2013-04-29	Merging Context and Sign.	ppedrot
2012-10-02	Remove the unused "intel" field in Proof.proof_state	letouzey
2012-08-08	Updating headers.	herbelin
2012-07-10	Small change in the printing of proofs for use by coqide.	aspiwack
2012-07-04	Change how the number of open goals is printed.	aspiwack
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey
2012-03-30	Added a command "Unfocused" which returns an error when the proof is	aspiwack
2012-03-20	Arranged for the desirable behaviour that bullets do not see beyond braces.	aspiwack