coq - The formal proof system

Age	Commit message (Expand)	Author
2018-06-27	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-12-30	Returning instance instead of substitution in universe context abstraction.	Pierre-Marie Pédrot
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-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-16	Clean up universes of constants and inductives	Amin Timany
2017-06-02	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross
2017-05-27	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias
2017-03-27	Adding the size of the opaquetab in its representation.	Pierre-Marie Pédrot
2017-03-27	Fix hashconsing of terms in the kernel.	Pierre-Marie Pédrot
2017-03-14	[future] Remove unused parameter greedy.	Emilio Jesus Gallego Arias
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-11	CLEANUP: kernel/context.ml{,i}	Matej Kosik
2015-10-28	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi
2015-01-12	Update headers.	Maxime Dénès
2014-10-13	library/opaqueTables: enable their use in interactive mode	Enrico Tassi
2014-08-03	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau
2014-05-06	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau
2014-05-06	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-25	Opaqueproofs: sink futures when interactive	Enrico Tassi
2014-02-26	Lazyconstr -> Opaqueproof	Enrico Tassi