| Age | Commit message (Expand) | Author |
|---|
| 2016-10-20 | Merge branch 'bug5036' into v8.6 | Matthieu Sozeau |
| 2016-10-20 | Fix bug #5036 autorewrite, sections and universes | Matthieu Sozeau |
| 2016-09-30 | Merge remote-tracking branch 'github/pr/299' into v8.6 | Maxime Dénès |
| 2016-09-29 | Fix bug #5036 autorewrite, sections and universes | Matthieu Sozeau |
| 2016-09-29 | Fix bug #4869, allow Prop, Set, and level names in constraints. | Matthieu Sozeau |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-06-18 | Reuse the typing_flags datatype for inductives. | Pierre-Marie Pédrot |
| 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-06-13 | Univs: more robust Universe/Constraint decls #4816 | Matthieu Sozeau |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 2016-01-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-23 | Fix bug #4503: mixing universe polymorphic and monomorphic | Matthieu Sozeau |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-15 | Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. | Maxime Dénès |
| 2016-01-14 | Changing "P is assumed" to "P is declared". | Hugo Herbelin |
| 2016-01-02 | Remove some useless type declarations. | Guillaume Melquiond |
| 2015-11-27 | Univs: entirely disallow instantiation of polymorphic constants with | Matthieu Sozeau |
| 2015-10-30 | Add a way to get the right fix_exn in external vernacular commands | Matthieu Sozeau |
| 2015-10-28 | Avoid type checking private_constants (side_eff) again during Qed (#4357). | Enrico Tassi |
| 2015-10-27 | Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names | Matthieu Sozeau |
| 2015-10-02 | Univs: Change intf of push_named_def to return the computed universe | Matthieu Sozeau |
| 2015-10-02 | Univs: refined handling of assumptions | Matthieu Sozeau |
| 2015-10-02 | Univs: fix Universe vernacular, fix bug #4287. | Matthieu Sozeau |
| 2015-09-25 | Propagate `Guarded` flag from syntax to kernel. | Arnaud Spiwack |
| 2015-09-23 | Hopefully better names to constructors of internal_flag, as discussed | Hugo Herbelin |
| 2015-06-24 | Add a corresponding field in `mutual_inductive_entry` (part 1). | Arnaud Spiwack |
| 2015-02-14 | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi |
| 2015-01-13 | Fix bug when discharging universe constraints coming from variables | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-05 | kernel/ind Change interface of declare_mind and declare_mutual | Matthieu Sozeau |
| 2014-11-23 | Pass around information on the use of template polymorphism for | Matthieu Sozeau |
| 2014-10-13 | STM: simplify how the term part of a side effect is retrieved | Enrico Tassi |
| 2014-10-13 | library/opaqueTables: enable their use in interactive mode | Enrico Tassi |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau |
| 2014-09-08 | Removing dead code relative to the XML plugin. | Pierre-Marie Pédrot |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | 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-07-25 | - Do module substitution inside mind_record. | Matthieu Sozeau |
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau |
| 2014-06-17 | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau |
| 2014-06-08 | ind_tables: always declare side effects (Closes: HOTT#110) | Enrico Tassi |
| 2014-05-16 | Declare: fix Future management | Enrico Tassi |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau |
