aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
Commit message (Expand)AuthorAge
* Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\
* | Renaming functions in Typing to stick to the standard e_* scheme.Gravatar Pierre-Marie Pédrot2016-02-15
| * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\|
| * (Partial) fix for bug #4453: raise an error instead of an anomaly.Gravatar Matthieu Sozeau2015-12-17
* | Fixing unexpected length of context in a typing function, detected byGravatar Hugo Herbelin2015-12-15
* | Unifying betazeta_applist and prod_applist into a clearer interface.Gravatar Hugo Herbelin2015-12-05
|/
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing a bug in the presence of let-in in inductive arity.Gravatar Hugo Herbelin2014-10-20
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 01:16:29 +0000