| Age | Commit message (Collapse) | Author |
|---|
|
If we remove all the legacy proof engine stuff, that would remove the
need for the view on proof almost entirely.
|
|
Add headers to a few files which were missing them.
|
|
|
|
We add the information on the proper layer by catching the low-level
exception.
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
|
`Vernacexpr` lives conceptually higher than `proof`, however,
datatypes for bullets and goal selectors are in `Vernacexpr`.
In particular, we move:
- `proof_bullet`: to `Proof_bullet`
- `goal_selector`: to a new file `Goal_select`
|
|
|
|
In particular `Proof_global.t` will become a first class object for
the upper parts of the system in a next commit.
|
|
|
|
Bullets were placed inside the `Proof_global` module, I guess that due
to the global registration function. However, it has logically nothing
to do with the functionality of `Proof_global` and the current
placement may create some interference between the developers
reworking proof state handling and bullets.
We thus put the bullet functionality into its own, independent file.
|
