diff options
| author | Maxime Dénès | 2017-11-30 16:21:37 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-30 16:21:37 +0100 |
| commit | e29993c250164b9486d4d7ffdebb9bfee4a2828f (patch) | |
| tree | 1d5014e9bec2aa05ed6bc9f231435ca4b3e7498d /parsing/g_proofs.ml4 | |
| parent | c5f6ee866bef4ff924693302ea98fec2b4742b9b (diff) | |
| parent | ae5944b360c1e181fa162d7d6dced7e671c6fbe6 (diff) | |
Merge PR #1049: Remove obsolete locality
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index f10d746770..d88f6fa0dc 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -70,19 +70,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 ] ] |