diff options
| author | Maxime Dénès | 2017-10-13 11:17:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-13 11:17:47 +0200 |
| commit | f8975f9fce08c7d43e6e57be980cfa36635969a9 (patch) | |
| tree | 6f5ea799e9ccc9e70354125a0bcd5977c1a10997 /parsing | |
| parent | 57bca928a3c0f7dc2582a4ffb8855ed668afdea2 (diff) | |
| parent | 4e016b91f59d3bb13681a53c35fbf4a979140b83 (diff) | |
Merge PR #1103: Take Suggest Proof Using outside the kernel.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 9 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 |
2 files changed, 3 insertions, 10 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 diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3e0b85b54a..a5b58b8553 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -580,8 +580,8 @@ GEXTEND Gram starredidentref: [ [ i = identref -> SsSingl i | i = identref; "*" -> SsFwdClose(SsSingl i) - | "Type" -> SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type") - | "Type"; "*" -> SsFwdClose (SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type")) ]] + | "Type" -> SsType + | "Type"; "*" -> SsFwdClose SsType ]] ; ssexpr: [ "35" |