aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.ml
AgeCommit message (Expand)Author
2019-03-18Merge PR #9740: Make NotConvertibleVect exception internal to typeopsPierre-Marie Pédrot
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-03-11Make NotConvertibleVect exception internal to typeopsGaëtan Gilbert
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-11-20Add a check that the return stack of an FProd is indeed empty.Pierre-Marie Pédrot
2018-11-20Use a closure for the domain argument of FProd.Pierre-Marie Pédrot
2018-11-20More efficient implementation of type_of_apply.Pierre-Marie Pédrot
2018-10-30Check univ instances in Typing.Gaëtan Gilbert
2018-10-26Merge PR #8684: Remove a few circumvolutions around parameters of inductive e...Gaëtan Gilbert
2018-10-26Remove a few circumvolutions around parameters of inductive entriesMaxime Dénès
2018-10-19Moving Global.constr_of_global_in_context to Typeops.Hugo Herbelin
2018-10-19Moving Global.type_of_global_in_context to Typeops.Hugo Herbelin
2018-10-16{Univops -> Vars}.universes_of_constrGaëtan Gilbert
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-07-25kernel: missing check that all universes are declared.Matthieu Sozeau
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-05-28Remove vm_conv hook and reorganize kernel filesMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-09-29Remove some duplication between Typeops and Nativenorm.Gaëtan Gilbert
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-04-11Update various comments to use "template polymorphism"Gaetan Gilbert
2016-12-12Replace Typeops by Fast_typeopsGaetan Gilbert
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-16Factorizing the uses of Declareops.safe_flags.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-02-16Renaming variants of Entries.local_entryMatej Kosik
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-10-18Miscellaneous typos, spacing, US spelling in comments or variable names.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:55:41 +0000