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 /API/API.mli | |
| 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 'API/API.mli')
| -rw-r--r-- | API/API.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index 04c69b025..879323a37 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4914,7 +4914,6 @@ module G_proofs : sig val hint : Vernacexpr.hints_expr Pcoq.Gram.entry - val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option end |