diff options
| author | Emilio Jesus Gallego Arias | 2018-11-16 20:16:41 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-21 01:26:45 +0100 |
| commit | 417641e48129c9ba8656c622c9b64cd32641e7de (patch) | |
| tree | bbd47886f4649999ecad9f21ffb6ff55869f0132 /dev/base_include | |
| parent | 968be14b3788e112425eedf696f2e5e35d35ba17 (diff) | |
[legacy proof engine] Remove some cruft.
We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.
This is not a lot but every little step helps.
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index 0e12b57b36..d2e8f6d092 100644 --- a/dev/base_include +++ b/dev/base_include @@ -135,7 +135,6 @@ open Pfedit open Proof open Proof_using open Proof_global -open Proof_type open Redexpr open Refiner open Tacmach |