diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 14 | ||||
| -rw-r--r-- | parsing/g_proofsnew.ml4 | 9 |
2 files changed, 16 insertions, 7 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 5acc694aa..5b2e165ac 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -87,17 +87,20 @@ GEXTEND Gram (* Hints for Auto and EAuto *) | IDENT "HintDestruct"; + local = locality; dloc = destruct_location; id = base_ident; hyptyp = Constr.constr_pattern; pri = natural; "["; tac = tactic; "]" -> - VernacHintDestruct (id,dloc,hyptyp,pri,tac) + VernacHintDestruct (local,id,dloc,hyptyp,pri,tac) - | IDENT "Hint"; hintname = base_ident; dbnames = opt_hintbases; ":="; h = hint - -> VernacHints (dbnames, h hintname) + | IDENT "Hint"; local = locality; hintname = base_ident; + dbnames = opt_hintbases; ":="; h = hint + -> VernacHints (local,dbnames, h hintname) - | IDENT "Hints"; (dbnames,h) = hints -> VernacHints (dbnames, h) + | IDENT "Hints"; local = locality; + (dbnames,h) = hints -> VernacHints (local,dbnames, h) (*This entry is not commented, only for debug*) @@ -106,6 +109,9 @@ GEXTEND Gram [Genarg.in_gen Genarg.rawwit_constr c]) ] ]; + locality: + [ [ IDENT "Local" -> true | -> false ] ] + ; hint: [ [ IDENT "Resolve"; c = Constr.constr -> fun name -> HintsResolve [Some name, c] | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c] diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4 index db8da7101..8cd36df1e 100644 --- a/parsing/g_proofsnew.ml4 +++ b/parsing/g_proofsnew.ml4 @@ -84,6 +84,7 @@ GEXTEND Gram (* Hints for Auto and EAuto *) | IDENT "HintDestruct"; + local = locality; dloc = destruct_location; id = base_ident; hyptyp = Constr.constr_pattern; @@ -91,10 +92,12 @@ GEXTEND Gram "["; tac = tactic; "]" -> VernacHintDestruct (id,dloc,hyptyp,pri,tac) - | IDENT "Hint"; hintname = base_ident; dbnames = opt_hintbases; ":="; h = hint - -> VernacHints (dbnames, h hintname) + | IDENT "Hint"; local = locality; hintname = base_ident; + dbnames = opt_hintbases; ":="; h = hint -> + VernacHints (dbnames, h hintname) - | IDENT "Hints"; (dbnames,h) = hints -> VernacHints (dbnames, h) + | IDENT "Hints"; local = locality; (dbnames,h) = hints -> + VernacHints (dbnames, h) (*This entry is not commented, only for debug*) |