aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
...
| * | | | | 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
|/ / /
| | * 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
| * | 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
|/ / /
| * | 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" work...Gravatar Maxime Dénès2017-09-15
|\ \
| | * weakens an hypothesis of Rle_RpowerGravatar Yves Bertot2017-09-06
| | * changed statements of Rpower_lt and Rle_power and addedGravatar Yves Bertot2017-09-06
* | | Addressing BZ#5713 (classical_left/classical_right artificially restricted).Gravatar Hugo Herbelin2017-09-03
| |/ |/|
* | A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
| * 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
* | | Fix typo in documentation for identityGravatar Tej Chajed2017-07-05
| |/ |/|
* | 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
| |/ |/|
| * plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
* | 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
| | * 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
| |/ / |/| |
* | | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| | * Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Gravatar Théo Zimmermann2017-06-08
| |/ |/|
* | drop vo.itarget files and compute the corresponding the corresponding values ...Gravatar Matej Kosik2017-06-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 07:19:23 +0000