| Commit message (Expand) | Author | Age |
* | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau | 2015-01-15 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau | 2014-09-09 |
* | Try a new way of handling template universe levels | Matthieu Sozeau | 2014-05-06 |
* | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | [Coercion]s use [Sortclass], not [Prop] (in docs) | Jason Gross | 2014-01-24 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Kills the useless tactic annotations "in |- *" | letouzey | 2012-07-05 |
* | ZArith + other : favor the use of modern names instead of compat notations | letouzey | 2012-07-05 |
* | No more use of tauto in Init/ | pboutill | 2012-01-19 |
* | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge | 2011-11-21 |
* | Arithemtic: more concerning compare, eqb, leb, ltb | letouzey | 2011-06-20 |
* | Modularization of BinNat + fixes of stdlib | letouzey | 2011-05-05 |
* | Better comments and organisation in Datatypes.v | letouzey | 2011-05-05 |
* | Init: some results in Type should rather be Defined than Qed | letouzey | 2011-03-21 |
* | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey | 2011-03-17 |
* | 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 |
* | Bool: iff lemmas about or, a reflect inductive, an is_true function | letouzey | 2010-07-10 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | CompSpec2Type is used to build functions, it should be Defined, not Qed | letouzey | 2010-02-13 |
* | CompSpecType, a clone of CompSpec but in Type instead of Prop | letouzey | 2010-02-12 |
* | Datatypes.length and app defined back via fun+fix instead of Fixpoint | letouzey | 2009-11-06 |
* | Better visibility of the inductive CompSpec used to specify comparison functions | letouzey | 2009-11-03 |
* | list, length, app are migrated from List to Datatypes | letouzey | 2009-11-02 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith | letouzey | 2009-07-24 |
* | Miscellaneous practical commits: | herbelin | 2009-06-29 |
* | Parsing files for numerals (+ ascii/string) moved into plugins | letouzey | 2009-03-27 |
* | Switched to "standardized" names for the properties of eq and | herbelin | 2009-01-01 |
* | - Optimized "auto decomp" which had a (presumably) exponential in | herbelin | 2008-12-26 |
* | Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b | herbelin | 2008-11-23 |
* | - Fixed minor bug #1994 in the tactic chapter of the manual [doc] | herbelin | 2008-11-22 |
* | - Patch sur "intros until 0" | herbelin | 2008-06-08 |
* | Notation concise pour la valeur par défaut des cas reconnus comme | herbelin | 2008-05-28 |
* | Added the automatic generation of the boolean equality if possible and the | vsiles | 2007-10-05 |
* | Déplacement des opérations sur bool dans l'état initial | herbelin | 2007-04-28 |
* | Mise en forme des theories | notin | 2006-10-17 |
* | Ajout d'alias pour prodT_rect et cie qui avaient été oublkÃiés | herbelin | 2006-05-29 |
* | - 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 |
* | Added option_map | herbelin | 2005-03-31 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Definition de la notation de la paire par un motif recursif | herbelin | 2004-03-17 |
* | Duplication temporaire des règles de syntaxe des paires | herbelin | 2003-12-16 |
* | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras | 2003-12-15 |
* | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin | 2003-11-29 |
* | Ajout lemme projections | herbelin | 2003-11-12 |