aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-23Merge PR #12552: Add a pre-hook mechanism for the `zify` tacticFrédéric Besson
Reviewed-by: fajb
2020-06-22Elementary properties about IZR for generic use.Hugo Herbelin
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-20Merge PR #12407: Fix #12406: fix Coq type error in dependent induction's LtacAnton Trunov
Reviewed-by: anton-trunov
2020-06-14Update zify documentationFrédéric Besson
Add Zify <X> are documented. Add <X> is deprecated as it clashed with the standard Add command
2020-06-14fix according to review by @pi8027Frédéric Besson
2020-06-14Update theories/micromega/ZifyBool.vFrédéric Besson
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com> - insert boolean constraint (b = true \/ b = false) - add specs for b2z - zify_post_hook performs a case-analysis over boolean constraints - Stricter typing constraints for `zify` declared operators The type is syntactically checked against the declaration of injections. Some explicit casts may need to be inserted.
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb.
2020-06-09Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.lebGuillaume Melquiond
Ack-by: Zimmi48 Reviewed-by: erikmd Reviewed-by: silene
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-06-08Fix 12483Pierre Roux
2020-05-25Fix #12406: fix Coq type error in dependent induction's LtacPaolo G. Giarrusso
2020-05-18Update to 8.13.Théo Zimmermann
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
2020-05-16Merge PR #12288: Prove that classical reals implement constructive reals.Michael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ↵Vincent Semeria
and max to CoRN. Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental
2020-05-15Move SSR's Search to a new plugin and deprecate it.Théo Zimmermann
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
Reviewed-by: Zimmi48 Reviewed-by: anton-trunov Reviewed-by: ejgallego
2020-05-12Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.leAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
2020-05-12Merge PR #12190: [stdlib] [Permutation] Declare more instances as GlobalAnton Trunov
Reviewed-by: JasonGross Reviewed-by: anton-trunov
2020-05-11Merge PR #10609: Register (for Coqlib.ref_lib) several base datatypes of stdlibHugo Herbelin
Reviewed-by: JasonGross
2020-05-10Merge PR #12287: Define CRzero and CRone via CR_of_QMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-09Hexadecimal: conversion to/from Coq stringsPierre Roux
2020-05-09Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijectionsPierre Roux
2020-05-09Add hexadecimal numeralsPierre Roux
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)
2020-05-09Decimal: prove numeral notation for QPierre Roux
Fill in the proofs, adding a few neessary lemmas along the way.
2020-05-09Decimal: specify numeral notation for QPierre Roux
2020-05-09Uniformize indentation in theories/NumbersPierre Roux
2020-05-09Define CRzero and CRone via CR_of_QVincent Semeria
Add real numbers up to 10
2020-05-09Merge PR #12237: [stdlib] [List] add results around incl, filter and nthHugo Herbelin
2020-05-09Merge PR #12122: Avoid registering as keywords the #... in PrimitiveMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: maximedenes
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
Reviewed-by: maximedenes
2020-05-09Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==Kazuhiko Sakaguchi
Reviewed-by: pi8027 Reviewed-by: zeldovich
2020-05-08Declare more Permutation instances as GlobalOlivier Laurent
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-07rename Bool.leb into Bool.le (same for ltb and compareb)Olivier Laurent
2020-05-07Merge PR #12024: Fixes for LaTeX/html export of standard library in coqdocThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-06Merge PR #12171: [stdlib] [list] Symmetry in conclusions of map_eq_cons and ↵Hugo Herbelin
map_eq_app Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-05-06Merge PR #12008: [stdlib] Add order properties about boolAnton Trunov
Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
Also `Export ExtrHaskellBasic` in `ExtrHaskellString`. Fixes #12257 Fixes #12258
2020-05-06Layout of Bool.v, especially for coqdoc.Hugo Herbelin
2020-05-06Adding properties about implb.Hugo Herbelin
This addresses a question on gitter (April 4).
2020-05-04add order properties about boolOlivier Laurent
2020-05-04add incl_Forall_in_iffOlivier Laurent
2020-05-04strenghten nth_extOlivier Laurent
2020-05-04add incl_map incl_filter NoDup_filterOlivier Laurent
2020-05-03Merge PR #12231: Simplify division of Cauchy realsMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-03consistency with PermutationOlivier Laurent
2020-05-03Simplify division of Cauchy realsVincent Semeria
Improve comments
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 17:11:19 +0000