coq/theories/PArith, 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
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 PArith/Pnat.v to compile with -mangle-names
2020-09-16T19:46:57+00:00

Jasper Hugunin

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

aa9f22f930a2207d5ff8e9ab88ddb08288245eee












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

Jasper Hugunin

2020-09-13T00:47:31+00:00

4185aebb3e47677752bc73b49705fd774461cbd8












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)







Avoiding using a fixed introduction name in Ltac code of stdlib.
2020-04-03T18:33:27+00:00

Hugo Herbelin

2020-03-22T11:30:55+00:00

aa889ee516453af65bd74ffedf8ec3761f97eb43












NArith, PArith: Add facts about iter
2020-03-31T20:24:16+00:00

Lysxia

2020-03-22T17:52:06+00:00

0fe509b865727db14277e672a120444d6b913449












Update headers in the whole code base.
2020-03-18T11:15:43+00:00

Théo Zimmermann

2020-03-18T11:14:26+00:00

a99776e10e0b2198d2b811ad82631111fb450f8a

Add headers to a few files which were missing them.





Add headers to a few files which were missing them.