coq - The formal proof system

Age	Commit message (Expand)	Author
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-03-14	Add a non-cumulative impredicative universe SProp.	Gaëtan Gilbert
2019-02-23	[vernac] Unify declaration hooks.	Emilio Jesus Gallego Arias
2018-11-30	[vernac] [hooks] Refactor towards optional hooks.	Emilio Jesus Gallego Arias
2018-11-17	[pfedit] Remove cook_proof stub.	Emilio Jesus Gallego Arias
2018-11-07	[Funind plugin] Remove some dead code	Vincent Laporte
2018-10-11	[vernac] Remove unused abstraction from declaration_hook type.	Emilio Jesus Gallego Arias
2018-06-18	Remove reference name type.	Maxime Dénès
2018-05-04	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias
2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
2017-10-17	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias
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-04-22	Merge branch v8.6 into trunk	Hugo Herbelin
2017-04-04	Solving first problem in bug #4306. TO DO : solve the let in problem	Julien Forest
2017-04-04	Merge branch 'trunk' into pr379	Maxime Dénès
2017-03-24	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin
2017-02-14	Funind API using EConstr.	Pierre-Marie Pédrot
2016-03-04	Rename Ephemeron -> CEphemeron.	Maxime Dénès
2015-10-28	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi
2015-04-14	Function now supports puniveres	jforest
2014-06-08	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot
2014-06-08	Enforce a correct exception handling in declaration_hooks	Enrico Tassi
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-12-04	Factoring(continued).	Arnaud Spiwack
2013-12-04	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack
2013-10-18	declaration_hooks use Ephemeron	gareuselesinge
2013-03-12	invalid_arg instead of raise (Invalid_argement ...)	letouzey
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-03-14	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau
2012-03-01	New version of recdef :	jforest
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2009-12-16	adding an option functional_induction_rewrite_dependent to make functional in...	jforest
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey