coq - The formal proof system

Age	Commit message (Expand)	Author
2019-11-01	Add primitive float computation in Coq kernel	Guillaume Bertholon
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-04	Primitive integers	Maxime Dénès
2018-10-15	Correct some spelling errors	Benjamin Barenblat
2018-09-24	[kernel] Compile with almost all warnings enabled.	Emilio Jesus Gallego Arias
2018-09-19	Merge PR #8447: Cleaning in the retroknowledge	Pierre-Marie Pédrot
2018-09-17	OCaml now exports the min and max non-constant tags, let's use it	Maxime Dénès
2018-09-17	[VM] Allocate a bit less in digits_from_uint	Maxime Dénès
2018-09-17	[VM] Inject structured constants in values without reallocating them.	Maxime Dénès
2018-09-17	[VM] Move structured_constant to Vmvalues	Maxime Dénès
2018-09-14	Retroknowledge: use GlobRef.t instead of Constr.t as entry	Vincent Laporte
2018-08-20	Do not inline let-bound functions in clambda optimization.	Pierre-Marie Pédrot
2018-07-24	VM: don't duplicate projection narg information in lproj/kproj	Gaëtan Gilbert
2018-07-24	Projections use index representation	Gaëtan Gilbert
2018-06-28	[env.env_rel_context.env_rel_ctx] -> [rel_context env]	Gaëtan Gilbert
2018-05-31	Reduce circular dependency constants <-> projections	Gaëtan Gilbert
2018-05-28	Fix #7333: vm_compute segfaults / Anomaly with cofix	Maxime Dénès
2018-05-28	Unify pre_env and env	Maxime Dénès
2018-05-23	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin
2018-04-02	[lib] Move global options to their proper place.	Emilio Jesus Gallego Arias
2018-03-03	Handling evars in the VM.	Pierre-Marie Pédrot
2018-02-23	New IR in VM: Clambda.	Maxime Dénès