index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-11-01
docs(gallina-extensions.rst): Say more on float literals extraction
Erik Martin-Dorel
2019-11-01
Communicate CFLAGS to dune
Pierre Roux
2019-11-01
Add some doc snippet in ExtrOCamlFloats.v
Erik Martin-Dorel
2019-11-01
Makefile.build: Fix rules of bin/votour{,.byte}
Erik Martin-Dorel
2019-11-01
Add extraction for primitive floats
Erik Martin-Dorel
2019-11-01
Add a check for gradual underflows
Pierre Roux
2019-11-01
Add the IEEE-754 arch requirement in INSTALL
Pierre Roux
2019-11-01
feat: Use SSE2_MATH if available & Die if missing on x87
Erik Martin-Dorel
2019-11-01
Fix ldshiftexp
Pierre Roux
2019-11-01
Add overlays
Pierre Roux
2019-11-01
docs: Add entry in changelog
Erik Martin-Dorel
2019-11-01
docs: Add refman+stdlib documentation
Erik Martin-Dorel
2019-11-01
Add "==", "<", "<=" in PrimFloat.v
Erik Martin-Dorel
2019-11-01
Make primitive float work on Windows
Pierre Roux
2019-11-01
Reimplement is_float
Pierre Roux
2019-11-01
Make primitive float work on x86_32
Pierre Roux
2019-11-01
Pretty-printing primitive float constants
Erik Martin-Dorel
2019-11-01
Parsing primitive float constants
Pierre Roux
2019-11-01
Add primitive floats to checker
Pierre Roux
2019-11-01
Add tests for primitive floats with 'native_compute'
Pierre Roux
2019-11-01
Add primitive floats to 'native_compute'
Pierre Roux
2019-11-01
Add next_{up,down} primitive float functions
Pierre Roux
2019-11-01
Implement classify on primitive float
Pierre Roux
2019-11-01
Change return type of primitive float comparison
Pierre Roux
2019-11-01
Put axioms on ldshiftexp and frshiftexp
Guillaume Bertholon
2019-11-01
Add tests for primitive floats with 'vm_compute'
Guillaume Bertholon
2019-11-01
Add primitive floats to 'vm_compute'
Guillaume Bertholon
2019-11-01
Add tests for primitive floats
Guillaume Bertholon
2019-11-01
Add Floats to standard library
Guillaume Bertholon
2019-11-01
Add primitive floats to Ltac2
Pierre Roux
2019-11-01
Add primitive float computation in Coq kernel
Guillaume Bertholon
2019-11-01
Declare type of primitives in CPrimitives
Pierre Roux
2019-10-31
Merge PR #11021: Fix build in master
Pierre-Marie Pédrot
2019-10-31
lra: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArith
Pierre-Marie Pédrot
2019-10-31
Merge PR #10985: Print argument info as an Arguments command in About
Emilio Jesus Gallego Arias
2019-10-31
[prettyp] remove `mod_ops` and `indirect_accessor` parameters
Gaëtan Gilbert
2019-10-31
Merge PR #10994: Numbers.Cyclic: use “lia” rather than “omega”
Pierre-Marie Pédrot
2019-10-31
Merge PR #10937: [stdlib]Reals: use “lia” rather than “omega”
Pierre-Marie Pédrot
2019-10-31
Merge PR #11000: make: guard cp calls with rm -f on executables
Pierre-Marie Pédrot
2019-10-31
Merge PR #9883: Add support for Sorts in numeral notations
Vincent Laporte
2019-10-31
Merge PR #10997: Implement the unsupported attribute error using the warning ...
Emilio Jesus Gallego Arias
2019-10-31
lia: depend only on ZArith_base
Vincent Laporte
2019-10-31
QArith: only depend on ZArith_base
Vincent Laporte
2019-10-31
Zdigits: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
Zquot: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
Zpow_facts: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
Zwf: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
Zgcd_alt: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
restore red behaviour printing
Gaëtan Gilbert
[next]