coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-02-26	Signed primitive integers	Ana
	Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal.
2020-11-05	Rename Dec and HexDec to Decimal and Hexadecimal	Pierre Roux
	As noted by Hugo Herbelin, Dec is rather used for "decidable".
2020-11-05	[numeral notation] Add support for parameterized inductives	Pierre Roux

2020-11-05	[numeral notation] Add tests for implicit arguments	Pierre Roux

2020-11-04	[numeral notation] Add tests for the via ... using ... option	Pierre Roux

2020-10-30	Renaming Numeral.v into Number.v	Pierre Roux

2020-09-11	Rename Numeral Notation command to Number Notation	Pierre Roux
	Keep Numeral Notation wit a deprecation warning.