aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2016-03-06Moving Eauto to a simple ML file.Pierre-Marie Pédrot
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-02-26Qcabs : absolute value on normalized rational numbers QcPierre Letouzey
2016-02-26Qcanon : fix names of lemmas Qcle_alt & Qcge_alt (were Qle_alt & Qge_alt)Pierre Letouzey
2016-02-26Qcanon : implement some old suggestions by C. AugerPierre Letouzey
2016-02-23Moving tauto.ml4 to a proper ML file.Pierre-Marie Pédrot
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot
2016-02-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-19Fixing bug #4582: cannot override notation [ x ].Pierre-Marie Pédrot
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Fix bug #4503: mixing universe polymorphic and monomorphicMatthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2016-01-13MMaps: remove it from final 8.5 release, since this new library isn't mature ...Pierre Letouzey
2016-01-05Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2015-12-31Put implicits back as in 8.4.Matthieu Sozeau
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-14Moved proof_admitted to its own file, named "AdmitAxiom.v".Maxime Dénès
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Fix to previous commit (ClassicalFacts.v).Hugo Herbelin
2015-12-05Adding proofs on the relation between excluded-middle and minimization.Hugo Herbelin
2015-12-05Experimenting removing strong normalization of the mid-statement in tactic cut.Hugo Herbelin
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-10Updating Compat85.v after bd1c97653 on bracketing last or-andHugo Herbelin
2015-11-07Adding an amazing property of Prop.Hugo Herbelin
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-03Update compatibility file for some of bug #4392Jason Gross
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-07Remove the "exists" overrides from Program. (Fix bug #4360)Guillaume Melquiond
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Remove Print Universe directive.Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-09-30Add compatibility files (feature 4319)Jason Gross
2015-09-09Merge remote-tracking branch 'origin/v8.5' into trunkHugo Herbelin
2015-09-08Emphasizing that eta for vectors is an instance of caseS, as pointedHugo Herbelin
2015-09-08Minor modifications to WeakFanTheorem.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 13:33:03 +0000