aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
AgeCommit message (Expand)Author
2021-04-06Typo in ChoiceFacts.Hugo Herbelin
2021-04-06Standardizing spacing for {| ... |} in two files.Hugo Herbelin
2021-01-08Modify Logic/ProofIrrelevanceFacts.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Logic/JMeq.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Logic/FunctionalExtensionality.v to compile with -mangle-namesJasper Hugunin
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-09-16Modify Logic/Eqdep_dec.v to compile with -vJasper Hugunin
2020-09-16Modify Logic/EqdepFacts.v to compile with -mangle-namesJasper Hugunin
2020-07-01UIP in SPropGaëtan Gilbert
2020-04-17Deprecate “omega”Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-12-14Being explicit on existence of a remote link.Hugo Herbelin
2019-11-13Register proof_irrelevancePierre Roux
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional extens...Hugo Herbelin
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria
2019-10-14ClassicalFacts.v: Unifying format for bibliographical references.Hugo Herbelin
2019-10-14Weak excluded-middle: adding a reference.Hugo Herbelin
2019-10-14Logic: Add equivalence between weak excluded-middle and classical Morgan's lawHugo Herbelin
2019-08-26Tauto: use Coqlib to locate “not” and “NNPP”Vincent Laporte
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-05-23Fixing typos - Part 3JPR
2019-04-02Remove -compat 8.7Jason Gross
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-03-14Add StrictProp.v with basic SProp related definitionsGaëtan Gilbert
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-11-19Merge PR #8987: Deprecate hint declaration/removal with no specified databasePierre-Marie Pédrot
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-11-01develop constructive epsilonVincent Semeria
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-02Update compat notations to be compat 8.7Jason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:21:37 +0000