aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Logic.v
AgeCommit message (Expand)Author
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
2014-05-07Removing comment outdated since eta holds in conversion rule (thisHugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-08-08Side effect free implementation of admit (Isabelle's oracle)gareuselesinge
2013-05-05Improving printing of 'rew' notationherbelin
2013-04-17Added group properties of eq_refl, eq_sym, eq_transherbelin
2012-11-15Some lemmas on property of rewriting. It will probably be worth atherbelin
2012-10-24Removed a few calls to "Opaque" in Logic.v ineffective since at leastherbelin
2012-08-08Updating headers.herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 22:14:04 +0000