aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Logic.v
Commit message (Expand)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-03-02
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Gravatar Hugo Herbelin2018-02-20
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Use the rew dependent notation in ex, ex2 proofsGravatar Jason Gross2017-05-28
* Make theorems about ex equality QedGravatar Jason Gross2017-05-28
* Make new proofs of equality QedGravatar Jason Gross2017-05-28
* Use extended notation for ex, ex2 typesGravatar Jason Gross2017-05-28
* Replace [ex'] with [ex]Gravatar Jason Gross2017-05-28
* Use [rew_] instead of [eq_rect_] prefixGravatar Jason Gross2017-05-28
* Add lemmas for ex2Gravatar Jason Gross2017-05-28
* Use [rew] notations rather than [eq_rect]Gravatar Jason Gross2017-05-28
* Add lemmas about equality of sigma typesGravatar Jason Gross2017-05-28
* Use [rew_] instead of [eq_rect_] prefixGravatar Jason Gross2017-05-28
* Use [rew] notations rather than [eq_rect]Gravatar Jason Gross2017-05-28
* Add more groupoid-like theorems about [eq]Gravatar Jason Gross2017-05-28
* Functional choice <-> [inhabited] and [forall] commuteGravatar Gaetan Gilbert2017-04-30
* Small typo in commentGravatar Vadim Zaliva2017-04-26
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\
* \ Merge PR#442: Allow interactive editing of Coq.Init.LogicGravatar Maxime Dénès2017-03-17
|\ \
* | | Compatibility of iff wrt not and imp.Gravatar Hugo Herbelin2017-03-03
| | * Fixing a little bug in printing ex2 (type was printed "_" by default).Gravatar Hugo Herbelin2017-02-23
| |/ |/|
| * Allow interactive editing of Coq.Init.LogicGravatar Jason Gross2017-02-21
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Remove Print Universe directive.Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Update headers.Gravatar Maxime Dénès2015-01-12
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
* Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Gravatar Hugo Herbelin2014-11-02
* Basic lemmas about the algebraic structure of equality.Gravatar Hugo Herbelin2014-05-31
* Removing comment outdated since eta holds in conversion rule (thisGravatar Hugo Herbelin2014-05-07
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Side effect free implementation of admit (Isabelle's oracle)Gravatar gareuselesinge2013-08-08
* Improving printing of 'rew' notationGravatar herbelin2013-05-05
* Added group properties of eq_refl, eq_sym, eq_transGravatar herbelin2013-04-17
* Some lemmas on property of rewriting. It will probably be worth atGravatar herbelin2012-11-15
* Removed a few calls to "Opaque" in Logic.v ineffective since at leastGravatar herbelin2012-10-24
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* "A -> B" is a notation for "forall _ : A, B".Gravatar pboutill2012-04-12
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
* No more use of tauto in Init/Gravatar pboutill2012-01-19
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Take benefit of bullets available by default in PreludeGravatar herbelin2011-08-10
* Less ambitious application of a notation for eq_rect. We proposedGravatar herbelin2011-08-10
* New proposition "rewrite Heq in H" for eq_rect (assuming that there isGravatar herbelin2011-08-08
* All the parameters of or can be implicits.Gravatar pboutill2011-07-26