| Age | Commit message (Expand) | Author |
|---|
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2011-11-18 | Restore backward compatibility. ":>" declares subinstances in Class declarati... | msozeau |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-01-19 | Les records déclarés avec Record ne peuvent plus être récursifs (le | aspiwack |
| 2009-01-17 | DISCLAIMER | puech |
| 2008-12-31 | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin |
| 2008-11-23 | Fixed bug #2006 (type constraint on Record was not taken into account) + | herbelin |
| 2008-11-10 | Fix mixup between Record, Structure and Class by adding a new variant for | msozeau |
| 2008-11-09 | More factorization of inductive/record and typeclasses: move class | msozeau |
| 2008-11-05 | Move Record desugaring to constrintern and add ability to use notations | msozeau |
| 2008-11-05 | Nouvelle syntaxe pour écrire des records (co)inductifs : | aspiwack |
| 2008-07-04 | Fixes in handling of implicit arguments: | msozeau |
| 2008-05-30 | Improvements on coqdoc by adding more information into .glob | msozeau |
| 2008-03-08 | Fix bugs that were reopened due to the change of setoid | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2005-02-18 | Moving centralised discharge into dispatched discharge_function; required to ... | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-01-02 | meilleure presentation des commentaires du traducteur | barras |
| 2003-09-06 | Mise en place possibilité de définitions locales dans les paramètres des r... | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-06-03 | Intgration uniforme de coercions dans les dclarations (Variable and co) et re... | herbelin |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2002-05-13 | Utilisation des de Bruijn pour la constructions des records et de leur projec... | herbelin |
| 2001-10-09 | Suppression des arguments sur les constantes, inductifs et constructeurs | barras |
| 2001-03-15 | entetes | filliatr |
| 2001-02-14 | Mise en place d'un système optionnel de discharge immédiat; prise en compte... | herbelin |
| 2001-01-24 | Prise en compte des noms longs dans les Hints et les Coercions, et réorganis... | herbelin |
| 2001-01-24 | Ajout de constantes locales dans les Records | herbelin |
| 2000-12-19 | Découpage des différentes fonctionnalités de build_mutual et definition_st... | herbelin |
| 2000-12-12 | syntaxe AST Inversion + commentaires ocamlweb autour de $ | filliatr |
| 2000-01-11 | Ajout de Record | herbelin |
| 1999-12-03 | - global_reference traite des variables | filliatr |
| 1999-12-02 | Version initiale | herbelin |
