coq - The formal proof system

Age	Commit message (Expand)	Author
2019-06-04	Proof_global: pass only 1 pstate when we don't want the proof stack	Gaëtan Gilbert
2019-05-24	Remove the indirect opaque accessor hooks from Opaqueproof.	Pierre-Marie Pédrot
2019-05-23	Fixing typos - Part 2	JPR
2019-03-27	[vernac] Allow path for `save_proof` where no proof state is present.	Emilio Jesus Gallego Arias
2019-03-27	[plugins] [funind] Adapt to removal of imperative proof state.	Emilio Jesus Gallego Arias
2019-03-20	Stop accessing proof env via Pfedit in printers	Maxime Dénès
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-08	Change interfaces of evarconv as suggested by Enrico.	Matthieu Sozeau
2019-02-04	Primitive integers	Maxime Dénès
2018-11-30	[vernac] [hooks] Refactor towards optional hooks.	Emilio Jesus Gallego Arias
2018-11-21	[legacy proof engine] Remove some cruft.	Emilio Jesus Gallego Arias
2018-11-19	Rename TranspState into TransparentState.	Pierre-Marie Pédrot
2018-11-19	Move transparent_state to its own module.	Pierre-Marie Pédrot
2018-11-02	Remove is_universe_polymorphism in funind	Gaëtan Gilbert
2018-10-30	Avoid redefining reduction functions in fun_ind	Maxime Dénès
2018-10-18	[universes] deprecate constr_of_global	Matthieu Sozeau
2018-10-15	Correct some spelling errors	Benjamin Barenblat
2018-10-10	[coqlib] Rebindable Coqlib namespace.	Emilio Jesus Gallego Arias
2018-05-28	Tactics.introduction: remove dangerous option ~check	Enrico Tassi
2018-05-25	Remove some occurrences of Evd.empty	Maxime Dénès
2018-05-24	[tactics] Remove anonymous fix/cofix form.	Emilio Jesus Gallego Arias
2018-05-23	[api] Move `opacity_flag` to `Proof_global`.	Emilio Jesus Gallego Arias
2018-05-17	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert
2018-05-14	Deprecate Typing.e_* functions	Gaëtan Gilbert
2018-05-11	Deprecate Evarconv.e_conv,e_cumul	Gaëtan Gilbert
2018-04-13	Evar maps contain econstrs.	Gaëtan Gilbert
2018-02-02	Reductionops.nf_* now take an environment.	Gaëtan Gilbert
2017-11-22	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias
2017-11-21	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias
2017-09-28	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot
2017-07-29	closing bug 5315	Julien Forest
2017-07-17	[funind] Remove spurious character in comment.	Emilio Jesus Gallego Arias
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias
2017-07-13	Safer API for Global.body_of_constant and variants.	Pierre-Marie Pédrot
2017-06-16	Removing Proof_type from the API.	Pierre-Marie Pédrot
2017-06-10	Remove (useless) aliases from the API.	Matej Košík
2017-06-07	Put all plugins behind an "API".	Matej Kosik
2017-06-06	Remove the Sigma (monotonous state) API.	Maxime Dénès
2017-06-02	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross
2017-05-31	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin
2017-05-29	Merge PR#512: [cleanup] Unify all calls to the error function.	Maxime Dénès
2017-05-27	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias
2017-05-27	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias
2017-04-27	Fix 4.04 warnings	Gaetan Gilbert
2017-04-27	Remove some unused values and types	Gaetan Gilbert
2017-04-22	Merge branch v8.6 into trunk	Hugo Herbelin
2017-04-04	end of correction of bug 4306	Julien Forest
2017-04-04	Bad correction in previous commit	Julien Forest
2017-04-04	Solving first problem in bug #4306. TO DO : solve the let in problem	Julien Forest
2017-03-24	Merge branch 'trunk' into pr379	Maxime Dénès