coq - The formal proof system

Age	Commit message (Expand)	Author
2020-09-18	Adding debugging printers for Intmap.	Hugo Herbelin
2020-08-27	[numeral] [plugins] Switch from `Big_int` to ZArith.	Emilio Jesus Gallego Arias
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-03	Merge PR #10390: UIP in SProp	Maxime Dénès
2020-07-02	Fix debug printer for auctx in presence of Anonymous	Gaëtan Gilbert
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-06-29	Moving the remaining Refiner functions to Tacmach.	Pierre-Marie Pédrot
2020-06-04	Move the cbn reduction to its own file, and simplify the RAKAM accordingly.	Pierre-Marie Pédrot
2020-04-21	Merge PR #11896: Use lists instead of arrays in evar instances.	Maxime Dénès
2020-04-15	[proof] Merge `Proof_global` into `Declare`	Emilio Jesus Gallego Arias
2020-04-06	Use lists instead of arrays in evar instances.	Pierre-Marie Pédrot
2020-03-22	Centralizing all kinds of numeral string management in numTok.ml.	Hugo Herbelin
2020-03-19	Merge PR #11795: Print implicit arguments in types of references	Hugo Herbelin
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-12	Print implicit arguments in types of references	SimonBoulier
2020-02-20	Adding a printer for GlobEnv in ocamldebug.	Hugo Herbelin
2020-01-30	Merge PR #11307: Remove the hacks relying on hardwired libobject tags.	Maxime Dénès
2019-12-22	Rename files with Class in their name to make their role clearer.	Pierre-Marie Pédrot
2019-12-22	Remove the hacks relying on hardwired libobject tags.	Pierre-Marie Pédrot
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-11-01	Add primitive float computation in Coq kernel	Guillaume Bertholon
2019-07-08	[api] Deprecate GlobRef constructors.	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-06-11	STM: encode in static types that vernac_when is only used when VtSideff	Gaëtan Gilbert
2019-06-04	VernacExtend produces vernac_interp_phase ADT (old name functional_vernac)	Gaëtan Gilbert
2019-06-04	Vernacextend only returns a proof_global.t option, not a vernacstate	Gaëtan Gilbert
2019-05-14	Merge PR #10164: Add aucontext debug printer	Pierre-Marie Pédrot
2019-05-14	Add aucontext debug printer	Gaëtan Gilbert
2019-05-13	Make detyping robust w.r.t. indexed anonymous variables	Maxime Dénès
2019-04-09	[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.	Emilio Jesus Gallego Arias
2019-03-28	Fix top_printers after removal of imperative state	Gaëtan Gilbert
2019-03-27	[vernac] 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-17	Separate variance and universe fields in inductives.	Gaëtan Gilbert
2019-02-04	Primitive integers	Maxime Dénès
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert
2018-11-17	[vernacextend] Consolidate extension points API	Emilio Jesus Gallego Arias
2018-11-13	[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.	Emilio Jesus Gallego Arias
2018-10-30	Generalizing the various evar_map printers in Termops over an environment.	Hugo Herbelin
2018-10-11	Merge PR #8161: Implement VERNAC EXTEND in coqpp	Maxime Dénès
2018-10-05	[kernel] Remove section paths from `KerName.t`	Maxime Dénès
2018-10-02	Pass unnamed arguments to ML macros.	Pierre-Marie Pédrot
2018-09-30	Typo in top_printers.ml.	Hugo Herbelin
2018-09-26	[print] Restrict use of "debug" Termops printer.	Emilio Jesus Gallego Arias
2018-06-28	Make Environ.globals abstract.	Gaëtan Gilbert
2018-06-26	Remove Sorts.contents	Gaëtan Gilbert
2018-06-18	Remove reference name type.	Maxime Dénès