| Age | Commit message (Expand) | Author |
|---|
| 2017-02-15 | [stm] Break stm/toplevel dependency loop. | Emilio Jesus Gallego Arias |
| 2016-11-03 | Lets Hints/Instances take an optional pattern | Matthieu Sozeau |
| 2016-06-18 | Reuse the typing_flags datatype for inductives. | Pierre-Marie Pédrot |
| 2016-06-16 | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive. | Pierre-Marie Pédrot |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-11 | CLEANUP: kernel/context.ml{,i} | Matej Kosik |
| 2015-09-14 | Univs: Add universe binding lists to definitions | Matthieu Sozeau |
| 2015-06-24 | Add corresponding field in `VernacInductive`. | Arnaud Spiwack |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-11-23 | Pass around information on the use of template polymorphism for | Matthieu Sozeau |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau |
| 2014-09-15 | Rework typeclass resolution and control of backtracking. | Matthieu Sozeau |
| 2014-09-04 | Remove [Infer] option of records. | Arnaud Spiwack |
| 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 |
