coq/theories/ZArith, branch masterThe formal proof systemRemove the omega tactic and related options2021-04-03T01:52:59+00:00Jim Fehrle2021-01-11T22:47:13+00:00d3a51ac24244f586dfeff1a93b68cb084370534e
Support locality attributes for Hint Rewrite (including export)2021-01-18T12:08:17+00:00Gaëtan Gilbert2021-01-07T12:55:23+00:004419a101a4f5a108be90cf4e420f0b6961e6caac
We deprecate unspecified locality as was done for Hint.
Close #13724
We deprecate unspecified locality as was done for Hint.
Close #13724
Modify ZArith/Zgcd_alt.v to compile with -mangle-names2020-12-16T04:37:36+00:00Jasper Hugunin2020-12-16T04:37:36+00:0025b41bb9f84a3420878a9284cd7c8cae7f4f4e5b
Modify ZArith/Zpow_facts.v to compile with -mangle-names2020-12-16T04:29:47+00:00Jasper Hugunin2020-12-16T04:29:47+00:00ecc7f595007b8fbd88c6e94108c7fcdea5ece312
Modify ZArith/Zpower.v to compile with -mangle-names2020-12-16T04:27:13+00:00Jasper Hugunin2020-12-16T04:27:13+00:0084da55bda44aa9e4891cfe1226bc18183df23bcf
Explicitly annotate all hint declarations of the standard library.2020-11-16T11:28:27+00:00Pierre-Marie Pédrot2020-11-14T16:55:07+00:0068cd077344ce37db1a601079dbc4fdcae6c8d41f
By default Coq stdlib warnings raise an error, so this is really required.
By default Coq stdlib warnings raise an error, so this is really required.
Merge PR #13173: Lint stdlib with -mangle-names #42020-11-09T08:07:27+00:00coqbot-app[bot]2020-11-09T08:07:27+00:00fcc82eaf6054cce65821fafafedd329dab732994
Reviewed-by: anton-trunov
Reviewed-by: anton-trunov
Rename Dec and HexDec to Decimal and Hexadecimal2020-11-04T23:20:53+00:00Pierre Roux2020-10-28T09:32:58+00:0036ac26532028bfc6f84e4dfc849b51f42a3d8286
As noted by Hugo Herbelin, Dec is rather used for "decidable".
As noted by Hugo Herbelin, Dec is rather used for "decidable".
Renaming Numeral.v into Number.v2020-10-30T13:11:19+00:00Pierre Roux2020-09-12T07:10:26+00:002d44c8246eccba7c1c452cbfbc6751cd222d0a6a
Modify ZArith/Znumtheory.v to compile with -mangle-names2020-10-12T02:05:14+00:00Jasper Hugunin2020-10-10T04:06:22+00:00db413d523cfe086cfe768232e465fee8fb51e17c