coq - The formal proof system

Age	Commit message (Expand)	Author
2020-09-01	Unify the shelves	Maxime Dénès
2020-08-31	Update update_global_env usage	Gaëtan Gilbert
2020-08-26	Move given_up goals to evar_map	Maxime Dénès
2020-08-24	Update sigma instead of erasing it in `update_global_env`	Maxime Dénès
2020-04-15	[proof] Move functions related to `Proof.t` to `Proof`	Emilio Jesus Gallego Arias
2020-04-15	[proof] Merge `Pfedit` into proofs.	Emilio Jesus Gallego Arias
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-07-11	[proof] Minor cleanup in proof.ml	Emilio Jesus Gallego Arias
2019-06-24	[proof] Move initial_euctx to proof_global	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
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