| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Proper nametab handling of global universe names |  Matthieu Sozeau | 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. |  Emilio Jesus Gallego Arias | 2017-11-06 |
| | | | | | We do up to `Term` which is the main bulk of the changes. | ||
| * | Allow declaring universe constraints at definition level. | Matthieu Sozeau | 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. |  Pierre-Marie Pédrot | 2017-07-04 |
| | | |||
| * | Put all plugins behind an "API". |  Matej Kosik | 2017-06-07 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |