aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.mli
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
* [summary] Adapt STM to the new Summary API.Gravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | | We need to a partial restore. I think that we could design a better API, but further work on the toplevel state should improve it progressively.
* [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| | | | | There don't really bring anything, we also correct some minor nits with the printing function.
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
|
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-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.
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* [vernac] Remove forward hooks from Obligations.Gravatar Emilio Jesus Gallego Arias2017-06-20
| | | | | | | This was (once again) a spurious inter-dependency, that we solve by introducing a new module with the proper functionality. This helps in cleaning up the code. Note that no code was changed, other than removing the setting of the references.
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
|
* Make Obligations see fix_exnGravatar Enrico Tassi2017-02-15
|
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.