aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-04Prevent double definition of Ltac2 constructors inside a module; Fix #11046Kenji Maillard
2019-11-04Prevent redefinition of Ltac2 types; fix #10097Kenji Maillard
2019-11-03Merge PR #10958: Elan → Stratego in documentation of `rewrite_strat`.Théo Zimmermann
Reviewed-by: Zimmi48
2019-11-03Elan → Stratego in documentation of `rewrite_strat`.Robbert Krebbers
@eelcovisser told me that the strategies in Luttik and Visser 97 were inspired by Elan, but they are not part of Elan. They are part of the Stratego language.
2019-11-02Merge PR #11007: [classes] Some refactoring on proof save preparation.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-11-01Merge PR #11028: Update the deprecation doc of `Shrink Obligations`Clément Pit-Claudel
2019-11-01Merge PR #10647: Expose universe processing in comInductive.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) ↵Enrico Tassi
relation Reviewed-by: gares
2019-11-01Update the deprecation doc of `Shrink Obligations`Jason Gross
Now it uses `.. deprecated` like all the other deprecation notices in the manual.
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes Ack-by: proux01 Ack-by: silene Ack-by: vbgl
2019-11-01minor cleanup of anonymous functionsGaëtan Gilbert
2019-11-01Expose universe processing in comInductive.Jan-Oliver Kaiser
2019-11-01Merge PR #8642: Compiled interfaces with -vos and -vok optionsPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-11-01Merge PR #11019: enforcing Ltac2 constructor name are uppercasedPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-01adding test file for Uppercase Ltac2 constructorsKenji Maillard
2019-11-01enforcing Ltac2 cosntructors name are uppercase in open typesKenji Maillard
2019-11-01Add warnings regarding the experimental nature of the vos feature in the doc.Pierre-Marie Pédrot
2019-11-01Teach coq_dune about the empty .vos produced by coqcGaëtan Gilbert
Without this the next dune command after build a vo will wipe out the vos, breaking interactive users. Also this means dune installs the .vos files.
2019-11-01[test-suite] acknowledge coq_mafile installs .vosEnrico Tassi
2019-11-01[make] install .vos along with .voEnrico Tassi
2019-11-01fix installation of vos files in coq Makefilecharguer
2019-11-01a tentative patch to allow interactive session to load .vos files; (recall ↵charguer
that the generation of a .vo files induces the creation of an empty .vos file.)
2019-11-01fix coq_makefile and doc for vos support.charguer
2019-11-01Changelog entryMaxime Dénès
2019-11-01additional details in the doc for -voscharguer
2019-11-01Implementing support for vos/vok files.charguer
A .vos file stores the result of compiling statements (defs, lemmas) but not proofs. A .vok file is an empty file that denotes successful compilation of the full contents of a .v file. Unlike a .vio file, a .vos file does not store suspended proofs, so it is more lightweight. It cannot be completed into a .vo file.
2019-11-01Merge PR #11015: [Nix] Update reference to nixpkgsThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-01docs(gallina-extensions.rst): Say more on float literals extractionErik Martin-Dorel
2019-11-01Communicate CFLAGS to dunePierre Roux
2019-11-01Add some doc snippet in ExtrOCamlFloats.vErik Martin-Dorel
(as suggested by @silene)
2019-11-01Makefile.build: Fix rules of bin/votour{,.byte}Erik Martin-Dorel
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
2019-11-01Add a check for gradual underflowsPierre Roux
2019-11-01Add the IEEE-754 arch requirement in INSTALLPierre Roux
Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
2019-11-01feat: Use SSE2_MATH if available & Die if missing on x87Erik Martin-Dorel
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
2019-11-01Fix ldshiftexpPierre Roux
* Fix the implementations and add tests * Change shift from int63 to Z (was always used as a Z) * Update FloatLemmas.v accordingly Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
2019-11-01Add overlaysPierre Roux
2019-11-01docs: Add entry in changelogErik Martin-Dorel
2019-11-01docs: Add refman+stdlib documentationErik Martin-Dorel
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
* Add a related test-suite in compare.v (generated by a bash script) Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
2019-11-01Make primitive float work on WindowsPierre Roux
2019-11-01Reimplement is_floatPierre Roux
is_float was relying on Obj.tag triggering a check that we are in the OCaml heap which is expensive. On extreme examples, this can lead to a global 2x speedup. Thanks to Maxime Dénès and Jacques-Henri Jourdan for their help in diagnosing this.
2019-11-01Make primitive float work on x86_32Pierre Roux
Flag -fexcess-precision=standard is not enough on x86_32 where -msse2 -mfpmath=sse is required (-msse is not enough) to avoid double rounding issues in the VM. Most floating-point operation are now implemented in C because OCaml is suffering double rounding issues on x86_32 with 80 bits extended precision registers used for floating-point values, causing double rounding making floating-point arithmetic incorrect with respect to its specification. Add a runtime test for double roundings.
2019-11-01Pretty-printing primitive float constantsErik Martin-Dorel
* map special floats to registered CRef's * kernel/float64.mli: add {is_infinity, is_neg_infinity} functions * kernel/float64.ml: Replace string_of_float with a safe pretty-printing function Namely: let to_string_raw f = Printf.sprintf "%.17g" f let to_string f = if is_nan f then "nan" else to_string_raw f Summary: * printing a binary64 float in 17 decimal places and parsing it again will yield the same float, e.g.: let f1 = 1. +. (0x1p-53 +. 0x1p-105) let f2 = float_of_string (to_string f1) f1 = f2 * OCaml's string_of_float gives a sign to nan values which shouldn't be displayed as all NaNs are considered equal here.
2019-11-01Parsing primitive float constantsPierre Roux
2019-11-01Add primitive floats to checkerPierre Roux
2019-11-01Add tests for primitive floats with 'native_compute'Pierre Roux
Tests are updated to include native computations.
2019-11-01Add primitive floats to 'native_compute'Pierre Roux
* Float added to is_value/get_value to avoid stack overflows (cf. #7646) * beware of the use of Array.map with floats (cf. comment in the makeblock function) NB: From here one, the configure option "-native-compiler no" is no longer needed.
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
2019-11-01Implement classify on primitive floatPierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 07:07:06 +0000