| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-12-06 | Merge PR #11127: Added theorem Nat.bezout_comm. | Hugo Herbelin | |
| Ack-by: Zimmi48 Ack-by: herbelin | |||
| 2019-12-05 | Added Nat.bezout_comm. | Daniel de Rauglaudre | |
| 2019-11-29 | Merge 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-26 | Fix #11039: proof of False with template poly and nonlinear universes | Gaë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-25 | PermutEq: use “lia” rather than “omega” | Vincent Laporte | |
| 2019-11-25 | PermutSetoid: use “lia” rather than “omega” | Vincent Laporte | |
| 2019-11-25 | MSets: use “lia” rather than “omega” | Vincent Laporte | |
| 2019-11-13 | Register proof_irrelevance | Pierre Roux | |
| 2019-11-11 | Run update-compat script with --release option. | Théo Zimmermann | |
| This should ideally have been done before the 8.11 branching. | |||
| 2019-11-01 | Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) ↵ | Enrico Tassi | |
| relation Reviewed-by: gares | |||
| 2019-11-01 | Fix ldshiftexp | Pierre 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-01 | docs: Add refman+stdlib documentation | Erik Martin-Dorel | |
| 2019-11-01 | Add "==", "<", "<=" in PrimFloat.v | Erik 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-01 | Pretty-printing primitive float constants | Erik 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-01 | Parsing primitive float constants | 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 | |
| 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-01 | Put axioms on ldshiftexp and frshiftexp | Guillaume 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-01 | Add Floats to standard library | Guillaume 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-31 | Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArith | Pierre-Marie Pédrot | |
| Ack-by: fajb Reviewed-by: ppedrot | |||
| 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 | |
| Reviewed-by: ppedrot | |||
| 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-30 | Numbers.Cyclic: use “lia” rather than “omega” | Vincent Laporte | |
| 2019-10-29 | Use a less kludgy way of solving #9114 | Jason Gross | |
| 2019-10-29 | Fix #9114, assert_succeeds (exact I) solves goal | Jason Gross | |
| 2019-10-29 | `assert_succeeds`&`assert_fails`: multisuccess fix | Jason Gross | |
| These tactics now work correctly with multisuccess tactics by wrapping the tactic argument in `once`. Fixes #10965 | |||
| 2019-10-28 | [stdlib]Reals: use “lia” rather than “omega” | Vincent Laporte | |
| 2019-10-27 | Merge PR #10827: Replace classical reals quotient axioms by functional ↵ | Hugo Herbelin | |
| extensionality Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin Ack-by: maximedenes | |||
| 2019-10-24 | Replace classical reals quotient axioms by functional extensionality. Define ↵ | Vincent Semeria | |
| homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers. | |||
| 2019-10-22 | FSetEqProperties: do not use “omega” | Vincent Laporte | |
| 2019-10-22 | OrderedTypeEx: do not use “omega” | Vincent Laporte | |
| 2019-10-22 | Zpower: do not use “omega” | Vincent Laporte | |
| 2019-10-22 | Qround: do not use “omega” | Vincent Laporte | |
| 2019-10-22 | Qreduction: do not use “omega” | Vincent Laporte | |
| 2019-10-22 | QArith_base: do not use “omega” | Vincent Laporte | |
| 2019-10-22 | FSets: do not use “omega” | Vincent Laporte | |
| 2019-10-22 | Znumtheory: do not use “omega” | Vincent Laporte | |
| 2019-10-22 | Zdiv: do not use “omega” | Vincent Laporte | |
| 2019-10-22 | Zcomplements: do not use “omega” | Vincent Laporte | |
| 2019-10-14 | ClassicalFacts.v: Unifying format for bibliographical references. | Hugo Herbelin | |
| 2019-10-14 | Weak excluded-middle: adding a reference. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |