aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Logic.v
AgeCommit message (Expand)Author
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-08-20Modify Init/Logic.v to compile with -mangle-names.Jasper Hugunin
2020-04-21Moving the main Require Export Ltac in Prelude.v.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-25Use implicit arguments in notations for eq.Gaëtan Gilbert
2020-02-19Choosing a standard format for the "rew dependent" notation.Hugo Herbelin
2019-12-26Add rew dependent NotationsJason Gross
2019-09-16Fix #10757: Program Fixpoint uses "exists" for telescopesGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
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-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-09-25Adding lemmas about dependent equality.Hugo Herbelin
2018-09-25Adding f_equal_dep in Logic.v.Hugo Herbelin
2018-07-10Fix typo in Init.Logic.whitequark
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
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-20Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-28Use the rew dependent notation in ex, ex2 proofsJason Gross
2017-05-28Make theorems about ex equality QedJason Gross
2017-05-28Make new proofs of equality QedJason Gross
2017-05-28Use extended notation for ex, ex2 typesJason Gross
2017-05-28Replace [ex'] with [ex]Jason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
2017-05-28Add lemmas for ex2Jason Gross
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
2017-05-28Add lemmas about equality of sigma typesJason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
2017-05-28Add more groupoid-like theorems about [eq]Jason Gross
2017-04-30Functional choice <-> [inhabited] and [forall] commuteGaetan Gilbert
2017-04-26Small typo in commentVadim Zaliva
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-17Merge PR#442: Allow interactive editing of Coq.Init.LogicMaxime Dénès
2017-03-03Compatibility of iff wrt not and imp.Hugo Herbelin
2017-02-23Fixing a little bug in printing ex2 (type was printed "_" by default).Hugo Herbelin
2017-02-21Allow interactive editing of Coq.Init.LogicJason Gross
2016-01-20Update copyright headers.Maxime Dénès
2015-10-02Remove Print Universe directive.Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-11-02Improving elimination with indices, getting rid of intrusive residualHugo Herbelin
2014-11-02Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Hugo Herbelin
2014-05-31Basic lemmas about the algebraic structure of equality.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:39:51 +0000