coq - The formal proof system

Age	Commit message (Expand)	Author
2019-11-01	Add primitive float computation in Coq kernel	Guillaume Bertholon
2019-09-29	Merge PR #10673: [lemmas] Cleanup users of default proof information.	Pierre-Marie Pédrot
2019-08-23	[lemmas] Cleanup users of default proof information.	Emilio Jesus Gallego Arias
2019-08-07	[funind] Move some exception-based control flow to explicit option typing.	Emilio Jesus Gallego Arias
2019-07-31	[funind] Port aux function to the new tactic engine.	Emilio Jesus Gallego Arias
2019-07-31	[funind] Move duplicated `observe_tac` function to indfun_common.	Emilio Jesus Gallego Arias
2019-07-08	[api] Deprecate GlobRef constructors.	Emilio Jesus Gallego Arias
2019-07-07	[error] Remove special error printing pre-processing	Emilio Jesus Gallego Arias
2019-07-01	[decls] Remove goal_object_kind type.	Emilio Jesus Gallego Arias
2019-07-01	[api] Refactor most of `Decl_kinds`	Emilio Jesus Gallego Arias
2019-06-26	[stm] [vernac] Remove special ?proof parameter from vernac main path	Emilio Jesus Gallego Arias
2019-06-24	[api] Move `locality` from `library` to `vernac`.	Emilio Jesus Gallego Arias
2019-06-24	[lemmas] [proof] Split proof kinds into per-layer components.	Emilio Jesus Gallego Arias
2019-06-24	[proof] Remove duplicated universe polymorphic from decl_kinds	Emilio Jesus Gallego Arias
2019-06-24	[lemmas] Turn Lemmas.info into a proper type with constructor.	Emilio Jesus Gallego Arias
2019-06-17	Allow to delay polymorphic opaque constants.	Pierre-Marie Pédrot
2019-06-12	[funind] Untabify; necessary to ease the review of subsequent work.	Emilio Jesus Gallego Arias
2019-06-09	[proof] Move proofs that have an associated constant to `Lemmas`	Emilio Jesus Gallego Arias
2019-06-08	Cleaning the status of Local Definition and similar.	Hugo Herbelin
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