coq/theories/Numbers/Natural/Abstract, branch master The formal proof system Support locality attributes for Hint Rewrite (including export) 2021-01-18T12:08:17+00:00 Gaëtan Gilbert 2021-01-07T12:55:23+00:00 4419a101a4f5a108be90cf4e420f0b6961e6caac We deprecate unspecified locality as was done for Hint. Close #13724 
We deprecate unspecified locality as was done for Hint.

Close #13724
Explicitly annotate all hint declarations of the standard library. 2020-11-16T11:28:27+00:00 Pierre-Marie Pédrot 2020-11-14T16:55:07+00:00 68cd077344ce37db1a601079dbc4fdcae6c8d41f 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.
Modify Numbers/Natural/Abstract/NBits.v to compile with -mangle-names 2020-09-16T19:46:57+00:00 Jasper Hugunin 2020-09-09T19:26:23+00:00 389cea0e7d930d62aa888f3fab902e9b3568a6f3 The bitwise tactic was performing `intros ?m`, and the name m got used later in many proofs. I defined a tactic notation `bitwise as m` to be able to provide the name for `m` explicitly. I did not make the notation local, because it seems like it would be useful for any clients using `bitwise` who want to avoid generated names. I have relatively little experience with writing Ltac and tactic notations, so if my solution can be improved, please show me how. 
The bitwise tactic was performing `intros ?m`, and the name m got
used later in many proofs. I defined a tactic notation `bitwise as m`
to be able to provide the name for `m` explicitly.

I did not make the notation local, because it seems like it would be
useful for any clients using `bitwise` who want to avoid generated
names.

I have relatively little experience with writing Ltac and tactic notations,
so if my solution can be improved, please show me how.
Modify Numbers/Natural/Abstract/NLcm.v to compile with -mangle-names 2020-09-16T19:46:57+00:00 Jasper Hugunin 2020-09-09T17:46:15+00:00 8710a9437442003681e838a36ae572b7b24a958e 






Modify Numbers/Natural/Abstract/NGcd.v to compile with -mangle-names
2020-09-16T19:46:57+00:00

Jasper Hugunin

2020-09-09T17:44:43+00:00

13a9a7f16acb520b1e38aeac9480f7d298a62bc7












Modify Numbers/Natural/Abstract/NDiv.v to compile with -mangle-names
2020-09-16T19:46:57+00:00

Jasper Hugunin

2020-09-09T17:41:35+00:00

2128f623d1d9f26b5791d65e95c8d624ac7e48b9












Modify Numbers/Natural/Abstract/NPow.v to compile with -mangle-names
2020-09-16T19:46:57+00:00

Jasper Hugunin

2020-09-09T17:39:41+00:00

6b677ba003748f6222539a083e9de7d47a60c373












Modify Numbers/Natural/Abstract/NParity.v to compile with -mangle-names
2020-09-16T19:46:57+00:00

Jasper Hugunin

2020-09-09T17:38:23+00:00

978a2ac4a3fa6bad0387115ba186b2f6041e1a1e












Modify Numbers/Natural/Abstract/NMaxMin.v to compile with -mangle-names
2020-09-16T19:46:57+00:00

Jasper Hugunin

2020-09-09T17:36:17+00:00

ffd6a5de785071485cf5b4623aa43defe614b083












Modify Numbers/Natural/Abstract/NSub.v to compile with -mangle-names
2020-09-16T19:46:57+00:00

Jasper Hugunin

2020-09-09T17:31:12+00:00

fd20085f6d073338b8c547f810f70baa9e414b28