coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-09	Replace cl_index with cl_typ in coercionops.ml	Kazuhiko Sakaguchi
2021-02-11	[vernac] pass the loc of the whole command to the interp function	Enrico Tassi
2021-01-07	Merge PR #13718: Move printing and sorting out of AcyclicGraph	coqbot-app[bot]
2021-01-06	Further pushing up the printing and sorting of universes.	Pierre-Marie Pédrot
2021-01-04	Change the representation of kernel case.	Pierre-Marie Pédrot
2020-12-28	Register a printer for fconstr substitutions in the kernel.	Pierre-Marie Pédrot
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-11-22	Adding debugging printer for stacks of EConstr.	Hugo Herbelin
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