| Commit message (Expand) | Author | Age |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | No more Coersion in Init. | Pierre Boutillier | 2014-04-10 |
* | Define [projT3] and [proj3_sig] | Jason Gross | 2014-04-10 |
* | Better unification for [projT1] and [proj1_sig]. | Jason Gross | 2013-12-12 |
* | Relaxing the constraint on eta-expanding on the fly while looking for | herbelin | 2013-05-05 |
* | Unset Asymmetric Patterns | pboutill | 2013-01-18 |
* | Updating headers. | herbelin | 2012-08-08 |
* | ZArith + other : favor the use of modern names instead of compat notations | letouzey | 2012-07-05 |
* | Bug 2767 | pboutill | 2012-05-09 |
* | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge | 2011-11-21 |
* | Same Implicit Arguments rule for sumbool and sumor. | pboutill | 2011-07-26 |
* | Init: some results in Type should rather be Defined than Qed | letouzey | 2011-03-21 |
* | Used multiple lists of implicit arguments to transfer the choices of | herbelin | 2010-10-23 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Some lemmas about dependent choice + extensions of Compare_dec + | herbelin | 2009-11-16 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | MAJ et bricoles diverses | herbelin | 2008-05-12 |
* | Une passe sur les réels: | herbelin | 2008-03-23 |
* | Ajout exist & cie à la table des hints par symétrie avec ex_intro & | herbelin | 2007-06-22 |
* | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin | 2006-05-28 |
* | Modification des propriétés (svn:executable) | notin | 2006-03-17 |
* | Documentation | herbelin | 2005-05-19 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | sumbool et sumor affich avec 'if' si possible | herbelin | 2004-04-06 |
* | Décomposition automatique des règles d'analyse syntaxique pour les | herbelin | 2004-02-12 |
* | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin | 2003-11-29 |
* | Passage des notations de type dans type_scope | herbelin | 2003-10-28 |
* | Commentaires | herbelin | 2003-10-23 |
* | Argument de except, error implicite seulement en v8; Changement 'as notation'... | herbelin | 2003-10-14 |
* | Argument implicite pour None, error, except | herbelin | 2003-10-13 |
* | Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type... | herbelin | 2003-09-23 |
* | Concentration des notations officielles dans Init/Notations; restructuration ... | herbelin | 2003-05-21 |
* | Activation des implicites pour la v8 | herbelin | 2003-04-09 |
* | Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiques | herbelin | 2002-11-26 |
* | Retablissement SynDef Value/Error | herbelin | 2002-11-25 |
* | Généralisation de l'utilisation de Notation | herbelin | 2002-11-24 |
* | option -dump-glob pour coqdoc | filliatr | 2002-02-14 |
* | changement generation de schema d'elimination, False_rec est primitif, Constr... | mohring | 2002-01-31 |
* | MAJ des Id pour coqweb | herbelin | 2002-01-09 |
* | Suppression d'Export redondants | herbelin | 2001-11-14 |
* | and_rec redondant | letouzey | 2001-09-27 |
* | Fin de la modif Exc/option | mohring | 2001-08-30 |
* | ajout option , Exc --> option, et lemmes dans les theories | mohring | 2001-08-29 |
* | Expérimentation de NewDestruct et parfois NewInduction | herbelin | 2001-08-05 |
* | documentation automatique de la bibliothèque standard | filliatr | 2001-04-11 |
* | Introduction d'une preuve de False_rec | mohring | 2001-03-30 |
* | entetes | filliatr | 2001-03-15 |
* | fichiers prelude Coq | filliatr | 1999-12-13 |