aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/typeops.ml
Commit message (Expand)AuthorAge
* Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
* Fix #4346 2/2: VM casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Univs: be more restrictive for template polymorphic constants: onlyGravatar Matthieu Sozeau2015-10-12
* Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* Fix typeops ignoring results of check functions with let _, and oneGravatar Matthieu Sozeau2015-02-10
* Update headers.Gravatar Maxime Dénès2015-01-12
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Quickly fixing bug #2996: typing functions now check when referring toGravatar Hugo Herbelin2014-06-28
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Reuse universe level substitutions for template polymorphism, fixing performanceGravatar 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
* Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.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
* Useless Array.to_list in Typeops.Gravatar Pierre-Marie Pédrot2014-03-10
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
* Delayed the computation of parameters in sort polymorphism ofGravatar herbelin2013-05-14
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* More informative error when a global reference is used in a context ofGravatar herbelin2013-02-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar 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
* Completing r14448 and thus continuing r14407 (using Cast to propagateGravatar herbelin2011-09-24
* Having added a special Cast for remembering the use of conversionGravatar herbelin2011-09-04
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
* Term_typing, Typeops: replace some generic '=' on constr by eq_constrGravatar puech2011-07-29
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Replaced printing number of ill-typed branch by printing name of constructorGravatar herbelin2011-04-08
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* 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
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Déplacement de on_judgment_type de Typeops vers TermopsGravatar herbelin2006-10-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 09:53:27 +0000