aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/indtypes.mli
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/
* Kernel: primitive projections handling of let-insGravatar Matthieu Sozeau2015-07-09
* Update headers.Gravatar Maxime Dénès2015-01-12
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Add test-suite file. Compute the name for the record binder in theGravatar Matthieu Sozeau2014-08-29
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Fixing #2846: Uncaught exception Reduction.NotArity.Gravatar ppedrot2013-08-04
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* - Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).Gravatar herbelin2009-01-11
* Fixed bug 1761 (unexpected anomaly when constructor type has invalidGravatar herbelin2008-01-05
* Nettoyage et standardisation des messages d'erreurs.Gravatar herbelin2007-05-17
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* entetesGravatar filliatr2001-03-15
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* - suppression mind_extract_paramsGravatar filliatr2000-12-15
* Les params d'inductif deviennent en même temps propre à chaque inductif d'u...Gravatar herbelin2000-12-14
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Ajouts des causes d'erreur de IndrecGravatar herbelin2000-05-18
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Prise en compte nouveau case_infoGravatar herbelin2000-03-21
* - environment -> safe_environmentGravatar filliatr1999-12-01
* deplacements des var. ex. hors du noyauGravatar filliatr1999-10-08
* ensembles de contraintes d'universGravatar filliatr1999-09-25
* ajout des inductifs (sans types singletons pour l'instant)Gravatar filliatr1999-08-30
* un petit effort de presentation dans les interfacesGravatar filliatr1999-08-30
* suppression champs inutiles dans constantes et inductifs; verification defini...Gravatar filliatr1999-08-27