aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2019-12-06additional statements on flat_mapOlivier Laurent
2019-12-06additional statements on map and ForallOlivier Laurent
2019-12-06integration of statements for nthOlivier Laurent
2019-12-06add elt_eq_unitOlivier Laurent
2019-12-06integration of statements for Exists and ForallOlivier Laurent
2019-12-06integration of list_sum and list_maxOlivier Laurent
2019-12-06integration of statements for repeatOlivier Laurent
2019-12-06integration of statements for NoDupOlivier Laurent
2019-12-06integration of additional statements for inclOlivier Laurent
2019-12-06integration of statements for removeOlivier Laurent
2019-12-06integration of statements for InOlivier Laurent
2019-12-06integration of statements for inclOlivier Laurent
2019-12-06integration of statements for revOlivier Laurent
2019-12-06integration of statements for concat and flat_mapOlivier Laurent
2019-12-06integration of statements for seqOlivier Laurent
2019-12-06integration of statements related to last elementOlivier Laurent
2019-12-06integration of Exists_or and Forall_andOlivier Laurent
2019-12-06redundancy between skipn_node and skipn_allOlivier Laurent
2019-12-05Added Nat.bezout_comm.Daniel de Rauglaudre
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ↵Emilio Jesus Gallego Arias
library Reviewed-by: ejgallego
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-26Remove `rapply` tactic notation in favor of just the tacticJason Gross
This increases backwards compatibility. If desired, we can add a tactic notation to simplify the spec of `rapply` in the future if we want.
2019-11-26Make rapply handle all numbers of underscoresJason Gross
Also add a tactic notation so that it takes in uconstrs by default. Also add some basic tests for `rapply`. Also document rapply in the manual
2019-11-26Remove some trailing whitespace in theories/Program/Tactics.vJason Gross
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes #10504.
2019-11-25PermutEq: use “lia” rather than “omega”Vincent Laporte
2019-11-25PermutSetoid: use “lia” rather than “omega”Vincent Laporte
2019-11-25MSets: use “lia” rather than “omega”Vincent Laporte
2019-11-13Register proof_irrelevancePierre Roux
2019-11-11Run update-compat script with --release option.Théo Zimmermann
This should ideally have been done before the 8.11 branching.
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) ↵Enrico Tassi
relation Reviewed-by: gares
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-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-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 next_{up,down} primitive float functionsPierre Roux
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
Replace `option comparison` with `float_comparison` (:= `FEq | FLt | FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid boxing and an extra match when using primitive float comparison.
2019-11-01Put axioms on ldshiftexp and frshiftexpGuillaume Bertholon
Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas. The shift value has been increased to 2 * emax + prec because in ldexp we want to be able to transform the smallest denormalized to the biggest float value in one call.
2019-11-01Add Floats to standard libraryGuillaume Bertholon
All supported floating point operations are defined on specification floats. Then we register the primitive type and functions, and add conversion functions to and from the specification type. Finally we put axioms to state that primitive operations behave exactly the same as specification operations. CREDITS: Most of the code inside SpecFloat is adapted from the Flocq library. NOTE: For the moment this code will not compile if native compilation is enabled in the configuration phase. This will be resolved later when native_compute will be supported by primitive floats. So please use option "-native-compiler no" in ./configure currently.
2019-10-31Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArithPierre-Marie Pédrot
Ack-by: fajb Reviewed-by: ppedrot
2019-10-31Merge PR #10994: Numbers.Cyclic: use “lia” rather than “omega”Pierre-Marie Pédrot
2019-10-31Merge PR #10937: [stdlib]Reals: use “lia” rather than “omega”Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-31lia: depend only on ZArith_baseVincent Laporte
2019-10-31QArith: only depend on ZArith_baseVincent Laporte
2019-10-31Zdigits: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zquot: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zpow_facts: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zwf: use “lia” rather than “omega”Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-25 12:59:52 +0000