| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2012-11-22 | Monomorphization (kernel) | ppedrot |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-09-24 | Completing r14448 and thus continuing r14407 (using Cast to propagate | herbelin |
| 2011-09-04 | Having added a special Cast for remembering the use of conversion | herbelin |
| 2011-08-10 | Propagated information from the reduction tactics to the kernel so | herbelin |
| 2011-07-29 | Term_typing, Typeops: replace some generic '=' on constr by eq_constr | puech |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
