Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Proper nametab handling of global universe names | 2017-12-01 | |
| | | | | | | | | They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced | ||
* | [api] Move structures deprecated in the API to the core. | 2017-11-06 | |
| | | | | We do up to `Term` which is the main bulk of the changes. | ||
* | Allow declaring universe constraints at definition level. | 2017-09-19 | |
| | | | | | | | | | | | | | | Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions. | ||
* | Bump year in headers. | 2017-07-04 | |
| | |||
* | Put all plugins behind an "API". | 2017-06-07 | |