aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2020-04-30do not re-export ListNotations from ProgramAntonio Nikishaev
2020-04-24Make the nsatz test-suite passJason Gross
2020-04-24[nsatz] Use Export rather than IncludeJason Gross
As per https://github.com/coq/coq/pull/12073#issuecomment-612869336
2020-04-24Split off Nsatz tactic part into NsatzTacticJason Gross
Closes #5445 Note that we use `Include` rather than `Export` to expose the machinery defined in `NsatzTactic` from `Nsatz` to preserve backwards compatibility with developments relying on absolute names of the constants previously defined in `Nsatz.v`.
2020-04-23Merge PR #12117: Make multiplication of Cauchy reals transparent and ↵Hugo Herbelin
accelerate it Reviewed-by: herbelin
2020-04-23Merge PR #12120: Fixing #12119 : remove useless hypothesis in ↵Hugo Herbelin
NoDup_Permutation_bis Reviewed-by: herbelin
2020-04-22Merge PR #12031: [stdlib] A library on cyclic permutations: CPermutationHugo Herbelin
Ack-by: Zimmi48 Ack-by: anton-trunov Reviewed-by: herbelin
2020-04-22Document Cauchy realsVincent Semeria
2020-04-21Moving the main Require Export Ltac in Prelude.v.Hugo Herbelin
2020-04-21Adding a Declare ML Module in empty file Ltac.v.Hugo Herbelin
Indeed, it would be intuitive that `Require Import Ltac` is an equivalent for Ltac of `Require Import Ltac2.Ltac2`. Also declaring the classic proof mode.
2020-04-21Merge PR #12014: [stdlib] Add properties of operations on vectorsHugo Herbelin
Reviewed-by: herbelin
2020-04-19A library on cyclic permutations: CPermutationOlivier Laurent
(following the pattern of Permutation.v)
2020-04-19Use binary integers for Cauchy realsVincent Semeria
2020-04-19remove useless hypothesis in NoDup_Permutation_bisOlivier Laurent
(thanks to new NoDup_incl_NoDup)
2020-04-18Make multiplication of Cauchy reals transparent and accelerate itVincent Semeria
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-17ZArith: move lia hints to a dedicated moduleVincent Laporte
2020-04-14Merge PR #11957: [stdlib] update sigma-type notationsHugo Herbelin
Reviewed-by: JasonGross Ack-by: herbelin
2020-04-11[dune] [stdlib] Build the standard library natively with Dune.Emilio Jesus Gallego Arias
This completes a pure Dune bootstrap of Coq. There is still the question if we should modify `coqdep` so it does output a dependency on `Init.Prelude.vo` in certain cases. TODO: We still double-add `theories` and `plugins` [in coqinit and in Dune], this should be easy to clean up. Setting `libs_init_load_path` does give a correct build indeed; however we still must call this for compatibility?
2020-04-11add properties of operations on vectorsOlivier Laurent
2020-04-10Merge PR #11882: Adding a short form of Ltac2 Fresh.freshPierre-Marie Pédrot
Reviewed-by: MSoegtropIMC Reviewed-by: ppedrot Ack-by: tchajed
2020-04-08Merge PR #12044: proposed fix for the issue #12015 (String_as_OT)Jason Gross
Reviewed-by: JasonGross
2020-04-08Merge PR #11909: Make the level of ≡ in Int63 consistent with =Hugo Herbelin
Reviewed-by: anton-trunov
2020-04-07Integrated changes proposed by @JasonGrossilya
2020-04-07proposed fix for the issue #12015 (String_as_OT)ilya
2020-04-03Avoiding using a fixed introduction name in Ltac code of stdlib.Hugo Herbelin
2020-04-01Merge PR #9803: Adding more trigonometry in RealsHugo Herbelin
Ack-by: MSoegtropIMC Ack-by: Zimmi48 Ack-by: herbelin
2020-04-01Merge pull request #11946 from olaure01/ollibs-permutationAnton Trunov
[stdlib] Add complementary results about Permutation
2020-04-01- Adjusted definitions and lemmas for asin and acos to what has been discussedMichael Soegtrop
- Added derivative for asin and acos - Added a few additional trigonometry lemmas - Added Lemmas for the derivative of a decreasing inverse function - Did some cleanup (move lemmas to the files where they belong)
2020-04-01- Addition to the Reals theory :thery
- minus: lemmas `Rminus_eq_0` and `Rmult_minus_distr_r` - sin : sin_inj - cos : cos_inj - sqrt : lemmas `pow2_sqrt` and `inv_sqrt` - atan : lemmas `tan_inj`, `atan_eq0`, `atan_tan` and `tan_atan` - asin : definition and some basic properties - acos : definition and some basic properties
2020-04-01Add complementary results about PermutationOlivier Laurent
2020-03-31NArith, PArith: Add facts about iterLysxia
2020-03-30Merge PR #11725: Cleanup stdlib reals.Hugo Herbelin
Ack-by: SkySkimmer Reviewed-by: herbelin
2020-03-30Missing apartness notationsVincent Semeria
2020-03-30new sig notations and spaces addedOlivier Laurent
2020-03-30Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”Maxime Dénès
Ack-by: Zimmi48 Reviewed-by: anton-trunov Ack-by: jfehrle Reviewed-by: maximedenes
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-27Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move ↵Vincent Semeria
ConstructiveReals into new directory Abstract. Remove imports of implementations inside those Abstract files. Add changelog for constructive reals cleanup Move Cauchy reals into new directory Cauchy Update stdlib index Rename sum_f_R0 Use coqdoc comments Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Improve notations
2020-03-27Merge PR #11848: Nicer printing for decimal constantsHugo Herbelin
Reviewed-by: herbelin
2020-03-26Merge PR #11885: Sorting: Swap the names of Sorted_sort and LocallySorted_sortHugo Herbelin
Reviewed-by: herbelin
2020-03-25Make the level of ≡ in Int63 consistent with =Jason Gross
Fixes #11905
2020-03-25Nicer printing for decimal constants in QPierre Roux
Print 1.5 as 1.5 and not 15e-1. We choose the shortest representation with tie break to the dot notation (0.01 rather than 1e-3). The printing remains injective, i.e. 12/10 is not mixed with 120/100, the first being printed as 1.2 and the last as 1.20.
2020-03-24“auto with zarith”: use “lia” rather than “omega”Vincent Laporte
2020-03-24[stdlib] Do not rely on failing “auto”Vincent Laporte
2020-03-23Fix levels of `<=?` and `<?` in the stdlibJason Gross
They were defined at level 70, no associativity in all but three places, where they were instead declared at level 35. Fixes #11890
2020-03-23Sorting: Swap the names of Sorted_sort and LocallySorted_sortLysxia
2020-03-21Add module ZifyPow to avoid compatibility issue with 8.11.Théo Zimmermann
Also tweak the changelog entry to explain the difference.
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2020-03-19Merge PR #11822: Grants #11692: clear dependent knows about let-inPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: ppedrot
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:11:34 +0000