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