aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/typeops.ml
Commit message (Expand)AuthorAge
* Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
* Remove vm_conv hook and reorganize kernel filesGravatar Maxime Dénès2018-05-28
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Remove some duplication between Typeops and Nativenorm.Gravatar Gaëtan Gilbert2017-09-29
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
* Replace Typeops by Fast_typeopsGravatar Gaetan Gilbert2016-12-12
* CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | Renaming variants of Entries.local_entryGravatar Matej Kosik2016-02-16
* | 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
* | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/ /
* | 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
| * Add a flag to deactivate guard checking in the kernel.Gravatar Arnaud Spiwack2015-06-26
|/
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 09:01:11 +0000