aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
Commit message (Expand)AuthorAge
* Delayed the computation of parameters in sort polymorphism ofGravatar herbelin2013-05-14
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* A more informative message when the elimination predicate forGravatar herbelin2013-02-17
* Moved code from Pretype_error to EvarutilGravatar ppedrot2013-02-10
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Taking into account the possibility of having a type of type which isGravatar herbelin2012-12-18
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Noise for nothingGravatar pboutill2012-03-02
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
* Still more unification in typing.mlGravatar herbelin2011-10-25
* More unification in type_of and addition of e_type_of to get the newGravatar herbelin2011-10-24
* Unification in the return clause of match was not supported in solve_evars.Gravatar herbelin2011-10-11
* Applied the trick of Chung-Kil Hur to solve second-order matchingGravatar herbelin2011-10-10
* 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
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Application de refresh_universes dans typing.ml et retyping.ml : lesGravatar herbelin2008-03-15
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* Unification des types + clause filtrage manquante + uniformisation localeGravatar herbelin2007-06-07
* Correction pour le rapport de bug #1325 par rétablissement duGravatar herbelin2007-01-22
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* Changement des named_contextGravatar gregoire2005-12-02
* essai de typage des instantiations d\'evarsGravatar barras2005-06-06
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* test de conversion laissait echapper exception NotConvertibleGravatar barras2004-05-14
* CommentairesGravatar herbelin2002-12-10
* Essai suppression nf_betaiota dans type_ofGravatar herbelin2002-12-09
* petite erreur dans le typage des let-inGravatar barras2002-03-28
* typage du produit: type_judgment appele avec contexte incorrectGravatar barras2002-02-19
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* Rétablissement de la persistance des Cast; typage des LetIn sans recours à ...Gravatar herbelin2001-11-08
* GROS COMMIT:Gravatar barras2001-11-05