aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/type_errors.mli
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* First attempt at a fix for guard condition on cofixpoints.Gravatar Maxime Dénès2014-07-22
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* More informative error when a global reference is used in a context ofGravatar herbelin2013-02-28
* Modulification of nameGravatar ppedrot2012-12-18
* Updating headers.Gravatar herbelin2012-08-08
* It happens that the type inference algorithm (pretyping) did not checkGravatar herbelin2011-10-05
* Replaced printing number of ill-typed branch by printing name of constructorGravatar herbelin2011-04-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
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Add more information to IllFormedRecBody exceptions, to show the exactGravatar msozeau2008-02-08
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Amélioration message d'erreur objet de récursion de type non inductifGravatar herbelin2004-08-06
* Nouvelle en-têteGravatar herbelin2004-07-16
* message d'erreur de garde des cofixGravatar barras2003-09-22
* - amelioration des messages d'erreur de la condition de gardeGravatar barras2002-12-18
* Amélioration messages d'erreur arité incorrecte (notamment record)Gravatar herbelin2001-11-21
* types vs constrGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Changement de la structure des points fixesGravatar barras2001-05-03
* entetesGravatar filliatr2001-03-15
* Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationGravatar herbelin2001-03-11
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Raffinement erreur Wrong PredicateGravatar herbelin2000-12-14
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* Ajout erreur GlobalNotFoundGravatar herbelin2000-11-20
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Messages d'erreurs CasesGravatar herbelin2000-10-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* kernel/type_errors.mlGravatar herbelin2000-09-06
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Normalisation des Evar avant génération des erreursGravatar herbelin2000-06-29
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* Ajouts des causes d'erreur de IndrecGravatar herbelin2000-05-18
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* Suppression Rel de rawconstr et correction de bugs d'affichageGravatar herbelin1999-12-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 08:15:38 +0000