coq/theories/NArith, 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
Merge PR #13173: Lint stdlib with -mangle-names #4 2020-11-09T08:07:27+00:00 coqbot-app[bot] 2020-11-09T08:07:27+00:00 fcc82eaf6054cce65821fafafedd329dab732994 Reviewed-by: anton-trunov 
Reviewed-by: anton-trunov
Rename Dec and HexDec to Decimal and Hexadecimal 2020-11-04T23:20:53+00:00 Pierre Roux 2020-10-28T09:32:58+00:00 36ac26532028bfc6f84e4dfc849b51f42a3d8286 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.v 2020-10-30T13:11:19+00:00 Pierre Roux 2020-09-12T07:10:26+00:00 2d44c8246eccba7c1c452cbfbc6751cd222d0a6a 






Modify NArith/Ndigits.v to compile with -mangle-names
2020-10-12T02:05:14+00:00

Jasper Hugunin

2020-10-09T23:54:33+00:00

44b13a7a3c5c849e6aca9a1f0a5e6aa0909fa651












Modify NArith/Nnat.v to compile with -mangle-names
2020-09-16T19:46:57+00:00

Jasper Hugunin

2020-09-13T01:01:56+00:00

9daa2ec464eb9b881cab7d53fd39efc5de3afe12












Modify NArith/BinNat.v to compile with -mangle-names
2020-09-16T19:46:57+00:00

Jasper Hugunin

2020-09-13T00:55:35+00:00

b7697c92cc1302c4860e4a4210e3699cabe3ca1b












Rename Numeral Notation command to Number Notation
2020-09-11T20:23:24+00:00

Pierre Roux

2020-09-09T21:33:05+00:00

6551f14196784e323688e682877229bc7f901659

Keep Numeral Notation wit a deprecation warning.





Keep Numeral Notation wit a deprecation warning.







Add hexadecimal numerals
2020-05-09T15:59:00+00:00

Pierre Roux

2020-03-26T07:20:09+00:00

692c642672f863546b423d72c714c1417164e506

We add hexadecimal numerals according to the following regexp
0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)?

This is unfortunately a rather large commit. I suggest reading it in
the following order:

* test-suite/output/ZSyntax.{v,out}       new test
* test-suite/output/Int63Syntax.{v,out}   ''
* test-suite/output/QArithSyntax.{v,out}  ''
* test-suite/output/RealSyntax.{v,out}    ''
* test-suite/output/FloatSyntax.{v,out}   ''

* interp/numTok.ml{i,}  extending numeral tokens

* theories/Init/Hexadecimal.v  adaptation of Decimal.v
                               for the new hexadecimal Numeral Notation
* theories/Init/Numeral.v  new interface for Numeral Notation (basically,
                           a numeral is either a decimal or an hexadecimal)

* theories/Init/Nat.v            add hexadecimal numeral notation to nat
* theories/PArith/BinPosDef.v    ''                                  positive
* theories/ZArith/BinIntDef.v    ''                                  Z
* theories/NArith/BinNatDef.v    ''                                  N
* theories/QArith/QArith_base.v  ''                                  Q

* interp/notation.ml{i,}     adapting implementation of numeral notations
* plugins/syntax/numeral.ml  ''

* plugins/syntax/r_syntax.ml  adapt parser for real numbers

* plugins/syntax/float_syntax.ml  adapt parser for primitive floats

* theories/Init/Prelude.v  register parser for nat
* adapting the test-suite (test-suite/output/NumeralNotations.{v,out}
  and test-suite/output/SearchPattern.out)
* remaining ml files (interp/constrex{tern,pr_ops}.ml where two open
  had to be permuted)





We add hexadecimal numerals according to the following regexp
0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)?

This is unfortunately a rather large commit. I suggest reading it in
the following order:

* test-suite/output/ZSyntax.{v,out}       new test
* test-suite/output/Int63Syntax.{v,out}   ''
* test-suite/output/QArithSyntax.{v,out}  ''
* test-suite/output/RealSyntax.{v,out}    ''
* test-suite/output/FloatSyntax.{v,out}   ''

* interp/numTok.ml{i,}  extending numeral tokens

* theories/Init/Hexadecimal.v  adaptation of Decimal.v
                               for the new hexadecimal Numeral Notation
* theories/Init/Numeral.v  new interface for Numeral Notation (basically,
                           a numeral is either a decimal or an hexadecimal)

* theories/Init/Nat.v            add hexadecimal numeral notation to nat
* theories/PArith/BinPosDef.v    ''                                  positive
* theories/ZArith/BinIntDef.v    ''                                  Z
* theories/NArith/BinNatDef.v    ''                                  N
* theories/QArith/QArith_base.v  ''                                  Q

* interp/notation.ml{i,}     adapting implementation of numeral notations
* plugins/syntax/numeral.ml  ''

* plugins/syntax/r_syntax.ml  adapt parser for real numbers

* plugins/syntax/float_syntax.ml  adapt parser for primitive floats

* theories/Init/Prelude.v  register parser for nat
* adapting the test-suite (test-suite/output/NumeralNotations.{v,out}
  and test-suite/output/SearchPattern.out)
* remaining ml files (interp/constrex{tern,pr_ops}.ml where two open
  had to be permuted)







Fixing #11903: Fixpoints not truly recursive in standard library.
2020-05-01T21:17:27+00:00

Hugo Herbelin

2020-04-19T11:00:09+00:00

df8df4637dfb4106854554cc2ac94b4fdd565e80

There was also a non truly recursive in the doc.





There was also a non truly recursive in the doc.