aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
AgeCommit message (Expand)Author
2018-06-05Merge PR #7690: Fixing typos in file Berardi.vPierre-Marie Pédrot
2018-06-04Deprecate implicit tactic solving.Pierre-Marie Pédrot
2018-06-03Fixing typos in file Berardi.vHugo Herbelin
2018-03-07[stdlib] Do not use “Require” inside sectionsVincent Laporte
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-27[stdlib] move “Require” out of sectionsVincent Laporte
2017-12-11Axiom-free proof of eta expansion.Jasper Hugunin
2017-09-03Addressing BZ#5713 (classical_left/classical_right artificially restricted).Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-10Remove remaining vo.itarget files (obsolete since PR #499)Pierre Letouzey
2017-05-03Reorganize comment documentation of ChoiceFacts.vGaetan Gilbert
2017-04-30Functional choice <-> [inhabited] and [forall] commuteGaetan Gilbert
2017-03-28Fixing missing PropFacts.v in Logic/vo.itarget.Hugo Herbelin
2017-03-24Merge PR#392: strengthened the statement of JMeq_eq_depMaxime Dénès
2017-03-19Add a forgotten (?) line to "theories/Logic/vo.itarget".Matej Kosik
2017-03-14Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eautoMaxime Dénès
2017-03-03Strengthening some of the results in ChoiceFacts.v.Hugo Herbelin
2017-03-03Adding explicitly a file to work in the context of propositional extensionality.Hugo Herbelin
2017-03-03Adding a file providing extensional choice (i.e. choice over setoids).Hugo Herbelin
2017-03-03Adding various properties and characterization of the extensionalHugo Herbelin
2017-03-03Slightly unifying renaming in ChoiceFacts.v.Hugo Herbelin
2017-03-03Logic library: Adding a characterization of excluded-middle in term ofHugo Herbelin
2017-03-03Formatting references with surrounding brackets in Diaconescu.v.Hugo Herbelin
2017-02-24Simplifying the proof of NoRetractToModalProposition.paradox inHugo Herbelin
2016-12-19Fix a typo in Hurkens.v commentJason Gross
2016-12-11strengthened the statement of JMeq_eq_depAbhishek Anand
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-10-08Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-06Fixing unexpected "noise" introduced in commit 24d5448c.Hugo Herbelin
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-02More tests for tactic "subst".Hugo Herbelin
2016-09-19extensionality: Handle dependently-used hypothesesJason Gross
2016-09-19Adding an "extensionality in H" tactic which applies functionalHugo Herbelin
2016-07-08Typo in a comment of stdlib.Hugo Herbelin
2016-02-22Moving the Tauto tactic to proper Ltac.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-20Update copyright headers.Maxime Dénès
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
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-05Fix to previous commit (ClassicalFacts.v).Hugo Herbelin
2015-12-05Adding proofs on the relation between excluded-middle and minimization.Hugo Herbelin
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-02 19:24:54 +0000