aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
...
* | | | | | Axiom-free proof of eta expansion.Gravatar Jasper Hugunin2017-12-11
| | | | | |
* | | | | | Remove most uses of function extensionality in Program.CombinatorsGravatar Jasper Hugunin2017-12-09
| | | | | |
| * | | | | Additional rewrite lemmas on Ensembles, in Powerset_factsGravatar Joachim Breitner2017-12-06
|/ / / / /
| | * | | proposed fix for issue #3213: extra variable m in Lt.S_predGravatar fredokun2017-12-01
| | | | |
* | | | | Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
| |/ / / |/| | |
| * | | Make list functions returning sumbools transparentGravatar Tej Chajed2017-11-15
|/ / / | | | | | | | | | Specifically Exists_dec, Forall_dec, and Forall_Exists_dec.
| | * Get rid of ' notation for Zpos in QArith.Gravatar Robbert Krebbers2017-11-14
| |/ |/|
* | Merge PR #1113: Adding 3 Arith/QArith lemmas that I found usefulGravatar Maxime Dénès2017-10-27
|\ \
| * | Chaining two tactics in a proofGravatar Raphaël Monat2017-10-27
| | |
| * | Moving from `is_true` to `= true`Gravatar Raphaël Monat2017-10-25
| | |
* | | Moving bug numbers to BZ# format in the source code.Gravatar Théo Zimmermann2017-10-19
| | | | | | | | | | | | | | | Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers.
| * | Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans.Gravatar Raphaël Monat2017-10-12
| | |
* | | Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Gravatar Maxime Dénès2017-10-10
|\ \ \
| | * | Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey.Gravatar Raphaël Monat2017-10-08
| | | |
| | * | Removed leb_not_le (already existing as Nat.leb_nle)Gravatar Raphaël Monat2017-10-08
| | | |
| * | | Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768)Gravatar Pierre Letouzey2017-10-07
| | | |
* | | | [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Gravatar Emilio Jesus Gallego Arias2017-10-05
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | The manual has long stated that these forms are deprecated. We add a warning for them, as indeed `Add Morphism` is an "proof evil" [*] command, and we may want to remove it in the future. We've also fixed the stdlib not to emit the warning. [*] https://ncatlab.org/nlab/show/principle+of+equivalence
| * | Changed the statement of leb_not_le; shortened the proofGravatar Raphaël Monat2017-10-03
| | |
| * | Add Qabs_Qinv: Qabs (/ q) == / (Qabs q).Gravatar Raphaël Monat2017-10-03
| | |
| * | Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x.Gravatar Raphaël Monat2017-10-03
| | |
| * | Add leb_not_le: (n <=? m) = false -> n > m.Gravatar Raphaël Monat2017-10-03
|/ /
* | Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵Gravatar Maxime Dénès2017-09-15
|\ \ | | | | | | | | | work better on them
| | * weakens an hypothesis of Rle_RpowerGravatar Yves Bertot2017-09-06
| | |
| | * changed statements of Rpower_lt and Rle_power and addedGravatar Yves Bertot2017-09-06
| | | | | | | | | | | | | | | | | | Rlt_Rpower_l and pow_INR. Unfortunately theorems Rpower_lt and Rle_power are named inconsistently, in spite of their similarity.
* | | Addressing BZ#5713 (classical_left/classical_right artificially restricted).Gravatar Hugo Herbelin2017-09-03
| |/ |/| | | | | | | As explained in BZ#5713 report, the requirement for a non-empty context is not needed, so we remove it.
* | A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation.
| * Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
|/
* Merge PR #882: Adding a V8.7 compatibility version number.Gravatar Maxime Dénès2017-07-26
|\
* \ Merge PR #885: Removing a dummy parameter in some FMapPositive statements.Gravatar Maxime Dénès2017-07-26
|\ \
* \ \ Merge PR #845: Add Z.mod_div lemma to standard library.Gravatar Maxime Dénès2017-07-26
|\ \ \
| | | * Adding a V8.7 compatibility version number.Gravatar Hugo Herbelin2017-07-21
| |_|/ |/| |
| | * Removing a dummy parameter in some FMapPositive statements.Gravatar Hugo Herbelin2017-07-16
| | | | | | | | | | | | | | | | | | The statements xelements_bits_lt_1 and xelements_bits_lt_2 had an unexpected extra dependency due to a name collision with a section variable.
* | | Fix typo in documentation for identityGravatar Tej Chajed2017-07-05
| |/ |/| | | | | Fixes Coq bug 5635 (https://coq.inria.fr/bugs/show_bug.cgi?id=5635).
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |
| * Fix Zmod_div.Gravatar Russell O'Connor2017-06-29
| |
| * Use forall for consistencyGravatar roconnor-blockstream2017-06-29
| |
| * Add Z.mod_div lemma to standard library.Gravatar Russell O'Connor2017-06-29
|/
* Merge PR#826: Put plugin exports in the right compatibility fileGravatar Maxime Dénès2017-06-26
|\
* \ Merge PR#794: Cleanup of ltac cmxsGravatar Maxime Dénès2017-06-23
|\ \
| | * Put plugin exports in the right compatibility fileGravatar Jason Gross2017-06-22
| |/ |/| | | | | | | | | | | | | This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607). PR #220 put the exports in the wrong compat files, presumably because it was originally targeted to version 8.6, and this wasn't updated when it was retargeted to version 8.7.
| * plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus : - wrong -for-pack used for their inner .cmx - dependency over modules not provided (for instance Tacenv, that ends up being a submodule of the pack ltac_plugin). But we were lucky, those files were actually never loaded, thanks to the several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin, and hence tell Coq that these modules are already known, preventing any attempt to load them. Anyway, this commit cleans up this mess (thanks PMP for the help)
* | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ | |/ |/|
* | Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Gravatar Maxime Dénès2017-06-14
|\ \
* | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
| | * Remove deprecated options from the standard library.Gravatar Guillaume Melquiond2017-06-14
| | |
| | * Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| |/ |/|
* | Merge PR#498: Bignums as a separate opam packageGravatar Maxime Dénès2017-06-14
|\ \
* \ \ Merge PR#385: Equality of sigma typesGravatar Maxime Dénès2017-06-13
|\ \ \
| | * | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| |/ / |/| | | | | | | | | | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
* | | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 10:08:31 +0000