aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Logic.v
AgeCommit message (Expand)Author
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
2012-04-12"A -> B" is a notation for "forall _ : A, B".pboutill
2012-04-06Fixing a few bugs (see #2571) related to interpretation of multiple bindersherbelin
2012-01-19No more use of tauto in Init/pboutill
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-08-10Take benefit of bullets available by default in Preludeherbelin
2011-08-10Less ambitious application of a notation for eq_rect. We proposedherbelin
2011-08-08New proposition "rewrite Heq in H" for eq_rect (assuming that there isherbelin
2011-07-26All the parameters of or can be implicits.pboutill
2011-07-16Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)herbelin
2011-07-16Added a characterization of unique existence.herbelin
2010-10-23Used multiple lists of implicit arguments to transfer the choices ofherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:07:13 +0000