aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.ml
AgeCommit message (Expand)Author
2015-10-15 Fix #4346 2/2: VM casts were not inferring universe constraints.Maxime Dénès
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-10-12Univs: be more restrictive for template polymorphic constants: onlyMatthieu Sozeau
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-06-26Add a flag to deactivate guard checking in the kernel.Arnaud Spiwack
2015-02-10Fix typeops ignoring results of check functions with let _, and oneMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-06-28Quickly fixing bug #2996: typing functions now check when referring toHugo Herbelin
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-05-09Reuse universe level substitutions for template polymorphism, fixing performanceMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Fix interface for template polymorphism, cleaning up code in all typing algor...Matthieu Sozeau
2014-05-06Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-10Useless Array.to_list in Typeops.Pierre-Marie Pédrot
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-02-28More informative error when a global reference is used in a context ofherbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-11-22Monomorphization (kernel)ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2011-09-24Completing r14448 and thus continuing r14407 (using Cast to propagateherbelin
2011-09-04Having added a special Cast for remembering the use of conversionherbelin
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-07-29Term_typing, Typeops: replace some generic '=' on constr by eq_constrpuech
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-08Replaced printing number of ill-typed branch by printing name of constructorherbelin
2010-12-18Univ.constraints made fully abstract instead of being a Set of abstract stuffletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-04-30Réutilisation de l'infrastructure pour le polymorphisme d'univers desherbelin
2008-04-27Correction du bug des types singletons pas sous-type de Setherbelin
2007-08-27Suppression des type_app et body_of_type qui alourdissent inutilement le codeherbelin
2006-10-29Compatibilité du polymorphisme de constantes avec les sections.herbelin
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2006-10-06Déplacement de on_judgment_type de Typeops vers Termopsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 03:40:06 +0000