| Age | Commit message (Expand) | Author |
|---|
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2017-12-09 | [lib] Rename Profile to CProfile | Emilio 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-29 | Remove some duplication between Typeops and Nativenorm. | Gaëtan Gilbert |
| 2017-07-26 | Removing template polymorphism for definitions. | Pierre-Marie Pédrot |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2017-06-16 | Clean up universes of constants and inductives | Amin Timany |
| 2017-06-02 | Drop '.' from CErrors.anomaly, insert it in args | Jason Gross |
| 2017-04-11 | Update various comments to use "template polymorphism" | Gaetan Gilbert |
| 2016-12-12 | Replace Typeops by Fast_typeops | Gaetan Gilbert |
| 2016-08-24 | CLEANUP: minor readability improvements | Matej Kosik |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-07-01 | Separate flags for fix/cofix/match reduction and clean reduction function names. | Maxime Dénès |
| 2016-06-18 | Moving the typing_flags to the environment. | Pierre-Marie Pédrot |
| 2016-06-16 | Factorizing the uses of Declareops.safe_flags. | Pierre-Marie Pédrot |
| 2016-06-16 | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive. | Pierre-Marie Pédrot |
| 2016-06-14 | Assume totality: dedicated type rather than bool | Arnaud Spiwack |
| 2016-02-16 | Renaming variants of Entries.local_entry | Matej Kosik |
| 2016-02-09 | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-11 | CLEANUP: kernel/context.ml{,i} | Matej Kosik |
| 2015-10-18 | Miscellaneous 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-15 | Fix #4346 1/2: native casts were not inferring universe constraints. | Maxime Dénès |
| 2015-10-12 | Univs: be more restrictive for template polymorphic constants: only | Matthieu Sozeau |
| 2015-07-10 | Option -type-in-type: added support in checker and making it contaminating | Hugo Herbelin |
| 2015-06-26 | Add a flag to deactivate guard checking in the kernel. | Arnaud Spiwack |
| 2015-02-10 | Fix typeops ignoring results of check functions with let _, and one | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-06-28 | Quickly fixing bug #2996: typing functions now check when referring to | Hugo Herbelin |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Fix interface for template polymorphism, cleaning up code in all typing algor... | Matthieu Sozeau |
| 2014-05-06 | Properly reinstate old-style polymorphism in the kernel and pretyping/retyping. | Matthieu Sozeau |
| 2014-05-06 | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-03-10 | Useless Array.to_list in Typeops. | Pierre-Marie Pédrot |
| 2013-12-30 | Support for evars and metas in native compiler. | Maxime Dénès |
| 2013-05-14 | Delayed the computation of parameters in sort polymorphism of | herbelin |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-02-28 | More informative error when a global reference is used in a context of | herbelin |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
