aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Specif.v
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* More uniform indentation of sigma lemmasGravatar Jason Gross2017-05-28
* Give explicit proof terms to proj2_sig_eq etc.Gravatar Jason Gross2017-05-28
* Add some more comments about sigma equalitiesGravatar Jason Gross2017-05-28
* Remove motive argument from [rew dependent]Gravatar Jason Gross2017-05-28
* Use a local [rew dependent] notationGravatar Jason Gross2017-05-28
* Add forward-chaining versions: [eq_sig*_uncurried]Gravatar Jason Gross2017-05-28
* Use notation for sigTGravatar Jason Gross2017-05-28
* Remove reference to [IsIso]Gravatar Jason Gross2017-05-28
* Use notations for [sig], [sigT], [sig2], [sigT2]Gravatar Jason Gross2017-05-28
* Use [rew_] instead of [eq_rect_] prefixGravatar Jason Gross2017-05-28
* Add equality lemmas for sig2 and sigT2Gravatar 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
* Functional choice <-> [inhabited] and [forall] commuteGravatar Gaetan Gilbert2017-04-30
* Add η principles for sigma typesGravatar Jason Gross2017-03-01
* Remove some trailing whitespace in Init/Specif.vGravatar Jason Gross2017-03-01
* Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
* Adding option "Set Reversible Pattern Implicit" to Specif.v so that anGravatar Hugo Herbelin2016-06-16
* Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Gravatar Hugo Herbelin2016-04-27
* Adding option "Set Reversible Pattern Implicit" to Specif.v so that anGravatar Hugo Herbelin2016-04-27
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Adding a notation { x & P } for { x : _ & P }.Gravatar Hugo Herbelin2015-08-02
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* No more Coersion in Init.Gravatar Pierre Boutillier2014-04-10
* Define [projT3] and [proj3_sig]Gravatar Jason Gross2014-04-10
* Better unification for [projT1] and [proj1_sig].Gravatar Jason Gross2013-12-12
* Relaxing the constraint on eta-expanding on the fly while looking forGravatar herbelin2013-05-05
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Bug 2767Gravatar pboutill2012-05-09
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Same Implicit Arguments rule for sumbool and sumor.Gravatar pboutill2011-07-26
* Init: some results in Type should rather be Defined than QedGravatar letouzey2011-03-21
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Some lemmas about dependent choice + extensions of Compare_dec +Gravatar herbelin2009-11-16
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* MAJ et bricoles diversesGravatar herbelin2008-05-12
* Une passe sur les réels:Gravatar herbelin2008-03-23
* Ajout exist & cie à la table des hints par symétrie avec ex_intro &Gravatar herbelin2007-06-22
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 06:48:58 +0000