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