diff options
| author | Emilio Jesus Gallego Arias | 2017-09-27 16:12:58 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-10-10 23:50:25 +0200 |
| commit | 7f1635816588ae200c8eed381d726bd29f57d899 (patch) | |
| tree | 305b8576ee8387385b80ef4ca07491739490aa38 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index e2c87bbbf6..f10d746770 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -17,12 +17,6 @@ open Pcoq.Vernac_ let thm_token = G_vernac.thm_token -let hint_proof_using e = function - | Some _ as x -> x - | None -> match Proof_using.get_default_proof_using () with - | None -> None - | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s))) - let hint = Gram.entry_create "hint" (* Proof commands *) @@ -35,8 +29,7 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c - | IDENT "Proof" -> - VernacProof (None,hint_proof_using G_vernac.section_subset_expr None) + | IDENT "Proof" -> VernacProof (None,None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Abort" -> VernacAbort None |