diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /parsing/g_proofs.ml4 | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'parsing/g_proofs.ml4')
-rw-r--r-- | parsing/g_proofs.ml4 | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 422384f3..70c5d5d8 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -88,7 +88,7 @@ GEXTEND Gram | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) - | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id) + | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id) | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) @@ -103,10 +103,9 @@ GEXTEND Gram (* Declare "Resolve" explicitly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; - pri = OPT [ "|"; i = natural -> i ]; - dbnames = opt_hintbases -> + info = hint_info; dbnames = opt_hintbases -> VernacHints (false,dbnames, - HintsResolve (List.map (fun x -> (pri, true, x)) lc)) + HintsResolve (List.map (fun x -> (info, true, x)) lc)) ] ]; obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] @@ -116,9 +115,8 @@ GEXTEND Gram | c = constr -> HintsConstr c ] ] ; hint: - [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; - pri = OPT [ "|"; i = natural -> i ] -> - HintsResolve (List.map (fun x -> (pri, true, x)) lc) + [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> + HintsResolve (List.map (fun x -> (info, true, x)) lc) | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) @@ -134,6 +132,8 @@ GEXTEND Gram | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ] ; mode: - [ [ l = LIST1 ["+" -> true | "-" -> false] -> l ] ] + [ [ l = LIST1 [ "+" -> ModeInput + | "!" -> ModeNoHeadEvar + | "-" -> ModeOutput ] -> l ] ] ; END |