coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-03	[build] Split stdlib to it's own opam package.	Emilio Jesus Gallego Arias
2021-02-26	Signed primitive integers	Ana
2021-01-04	Remember universe instances of constants in notations	Jasper Hugunin
2020-12-02	Merge PR #13275: Put all Int63 primitives in a separate file	Vincent Laporte
2020-12-02	Put all Int63 primitives in a separate file	Pierre Roux
2020-11-05	[string notation] Handle parameterized inductives and non inductives	Pierre Roux
2020-11-05	Merge numeral and string notation plugins	Pierre Roux
2020-11-05	[numeral notation] Add support for parameterized inductives	Pierre Roux
2020-11-05	[numeral notation] Handle implicit arguments	Pierre Roux
2020-11-05	[numeral notation] R	Pierre Roux
2020-11-04	[numeral notation] Adding the via ... using ... option	Pierre Roux
2020-11-04	[numeral notation] Add a pre/postprocessing	Pierre Roux
2020-10-30	Renaming Numeral into Number	Pierre Roux
2020-10-30	Renaming numnotoption into number_modifier	Pierre Roux
2020-10-30	Renaming Numeral.v into Number.v	Pierre Roux
2020-10-27	Rename misc nonterminals	Jim Fehrle
2020-09-11	Rename Numeral Notation command to Number Notation	Pierre Roux
2020-08-27	[numeral] [plugins] Switch from `Big_int` to ZArith.	Emilio Jesus Gallego Arias
2020-05-19	[primitive floats] Add low level hexadecimal printing	Pierre Roux
2020-05-09	Add hexadecimal numerals	Pierre Roux
2020-05-09	Rename functions	Pierre Roux
2020-04-11	[dune] [stdlib] Build the standard library natively with Dune.	Emilio Jesus Gallego Arias
2020-03-29	Merge PR #11859: Warn when non exactly parsing non floating-point	Hugo Herbelin
2020-03-26	Print a warning when parsing non floating-point values.	Pierre Roux
2020-03-25	Nicer printing for decimal constants in R	Pierre Roux
2020-03-22	Centralizing all kinds of numeral string management in numTok.ml.	Hugo Herbelin
2020-03-22	Adding bignat to parse positive numbers; bigint now includes negative ints.	Hugo Herbelin
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-10	Fixing little bug in parsing decimal numbers in R.	Hugo Herbelin
2020-01-28	Fix #11467	Pierre Roux
2019-11-01	Parsing primitive float constants	Pierre Roux
2019-10-24	Replace classical reals quotient axioms by functional extensionality. Define ...	Vincent Semeria
2019-08-19	[api] Move handling of variable implicit data to impargs	Emilio Jesus Gallego Arias
2019-07-16	Define constructive real numbers as Cauchy sequences of rational numbers. Red...	Vincent Semeria
2019-07-08	[api] Deprecate GlobRef constructors.	Emilio Jesus Gallego Arias
2019-06-17	Update headers of files that were stuck on older headers.	Théo Zimmermann
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-24	Use global env in numeral and string notations	Maxime Dénès
2019-05-03	Fix #10054: Numeral Notations without the ltac plugin.	Pierre-Marie Pédrot
2019-04-02	Make R parser parse decimals (e.g., 1.02e+01)	Pierre Roux
2019-04-02	Add parsing of decimal constants (e.g., 1.02e+01)	Pierre Roux
2019-03-27	[coqpp] [ltac] 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-02-04	Primitive integers	Maxime Dénès
2019-01-25	[Numeral notations] Lazy resolution of decimal types	Vincent Laporte
2019-01-25	[Numeral notations] Use Coqlib registered constants	Vincent Laporte
2018-11-28	Factor out common code in numeral/string notations	Jason Gross
2018-11-28	Add `String Notation` vernacular like `Numeral Notation`	Jason Gross
2018-11-07	[R syntax plugin] Remove some dead code	Vincent Laporte
2018-11-02	coqpp VERNAC EXTEND uses #[ att = attribute; ] syntax	Gaëtan Gilbert