aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
Commit message (Expand)AuthorAge
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Proofview refiner is now type-safe by default.Gravatar Pierre-Marie Pédrot2014-09-04
* Typing.sort_of does not leak evarmaps anymore.Gravatar Pierre-Marie Pédrot2014-09-04
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Quickly fixing bug #2996: typing functions now check when referring toGravatar Hugo Herbelin2014-06-28
* Change interface of refresh universes to get a pbty argument instead ofGravatar Matthieu Sozeau2014-06-26
* - Add an option to refresh only algebraic universes, for e_type_of. The goalGravatar Matthieu Sozeau2014-06-21
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Refresh universes for Ltac's type_of, as the term can be used anywhere,Gravatar Matthieu Sozeau2014-05-09
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Fix interface for template polymorphism, cleaning up code in all typing algor...Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* 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
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 21:59:13 +0000