diff options
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index f10d746770..1c3ba78376 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -28,7 +28,8 @@ GEXTEND Gram | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ] ; command: - [ [ IDENT "Goal"; c = lconstr -> VernacGoal c + [ [ IDENT "Goal"; c = lconstr -> + VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((Loc.tag ~loc:!@loc Names.Anonymous), None), ProveBody ([], c)) | IDENT "Proof" -> VernacProof (None,None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; c = lconstr -> VernacExactProof c @@ -70,19 +71,16 @@ GEXTEND Gram VernacCreateHintDb (id, b) | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> VernacRemoveHints (dbnames, ids) - | IDENT "Hint"; local = obsolete_locality; h = hint; + | IDENT "Hint"; h = hint; dbnames = opt_hintbases -> - VernacHints (local,dbnames, h) + VernacHints (dbnames, h) (* Declare "Resolve" explicitly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info; dbnames = opt_hintbases -> - VernacHints (false,dbnames, + VernacHints (dbnames, HintsResolve (List.map (fun x -> (info, true, x)) lc)) ] ]; - obsolete_locality: - [ [ IDENT "Local" -> true | -> false ] ] - ; reference_or_constr: [ [ r = global -> HintsReference r | c = constr -> HintsConstr c ] ] |