diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-27 16:12:58 +0200 |
---|---|---|
committer | Gaƫtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-10 23:50:25 +0200 |
commit | 7f1635816588ae200c8eed381d726bd29f57d899 (patch) | |
tree | 305b8576ee8387385b80ef4ca07491739490aa38 /proofs/proofs.mllib | |
parent | ffc91e6fcc7a1f3d719b7ad95dbbd3293e26c653 (diff) |
[vernac] Remove "Proof using" hacks from parser.
We place `Proof_using` in the proper place [`vernac`] and we remove
gross parsing hacks.
The new placement should allow to use the printers and more convenient
structure, and reduce strange coupling between parsing and internal
representation.
Diffstat (limited to 'proofs/proofs.mllib')
-rw-r--r-- | proofs/proofs.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index eaf0c693e..058e839b4 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,7 +1,6 @@ Miscprint Goal Evar_refiner -Proof_using Proof_type Logic Refine |