aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2018-02-20Trying a hack to support {'pat|P} without breaking compatibility.Hugo Herbelin
2018-02-20Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Hugo Herbelin
2018-02-20More structured printing in unicode notations for binders.Hugo Herbelin
2018-02-20User-level support for Gonthier-Ssreflect's "if t then pat then u else v".Hugo Herbelin
2018-02-19Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Maxime Dénès
2018-02-12Merge PR #6139: Make list functions returning sumbools transparentMaxime Dénès
2018-01-08Document between and exists_between types.Ismail
2018-01-06Remove dir-locals and ship suggested helper hooks instead.Gaëtan Gilbert
2017-12-19Fix warning about shadowing a global name.Gaëtan Gilbert
2017-12-14Add named timers to LtacProfJason Gross
2017-12-12Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_factsMaxime Dénès
2017-12-11Axiom-free proof of eta expansion.Jasper Hugunin
2017-12-09Remove most uses of function extensionality in Program.CombinatorsJasper Hugunin
2017-12-06Additional rewrite lemmas on Ensembles, in Powerset_factsJoachim Breitner
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-15Make list functions returning sumbools transparentTej Chajed
2017-10-27Merge PR #1113: Adding 3 Arith/QArith lemmas that I found usefulMaxime Dénès
2017-10-27Chaining two tactics in a proofRaphaël Monat
2017-10-25Moving from `is_true` to `= true`Raphaël Monat
2017-10-19Moving bug numbers to BZ# format in the source code.Théo Zimmermann
2017-10-12Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans.Raphaël Monat
2017-10-10Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Maxime Dénès
2017-10-08Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey.Raphaël Monat
2017-10-08Removed leb_not_le (already existing as Nat.leb_nle)Raphaël Monat
2017-10-07Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768)Pierre Letouzey
2017-10-05[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Emilio Jesus Gallego Arias
2017-10-03Changed the statement of leb_not_le; shortened the proofRaphaël Monat
2017-10-03Add Qabs_Qinv: Qabs (/ q) == / (Qabs q).Raphaël Monat
2017-10-03Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x.Raphaël Monat
2017-10-03Add leb_not_le: (n <=? m) = false -> n > m.Raphaël Monat
2017-09-15Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...Maxime Dénès
2017-09-03Addressing BZ#5713 (classical_left/classical_right artificially restricted).Hugo Herbelin
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-26Merge PR #882: Adding a V8.7 compatibility version number.Maxime Dénès
2017-07-26Merge PR #885: Removing a dummy parameter in some FMapPositive statements.Maxime Dénès
2017-07-26Merge PR #845: Add Z.mod_div lemma to standard library.Maxime Dénès
2017-07-21Adding a V8.7 compatibility version number.Hugo Herbelin
2017-07-16Removing a dummy parameter in some FMapPositive statements.Hugo Herbelin
2017-07-05Fix typo in documentation for identityTej Chajed
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-29Fix Zmod_div.Russell O'Connor
2017-06-29Use forall for consistencyroconnor-blockstream
2017-06-29Add Z.mod_div lemma to standard library.Russell O'Connor
2017-06-26Merge PR#826: Put plugin exports in the right compatibility fileMaxime Dénès
2017-06-23Merge PR#794: Cleanup of ltac cmxsMaxime Dénès
2017-06-22Put plugin exports in the right compatibility fileJason Gross
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-14Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 20:00:26 +0000