aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.ml
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:18:53 +0000