diff options
| -rw-r--r-- | parsing/g_proofsnew.ml4 | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4 index 8cd36df1ec..82896099f8 100644 --- a/parsing/g_proofsnew.ml4 +++ b/parsing/g_proofsnew.ml4 @@ -90,14 +90,14 @@ GEXTEND Gram hyptyp = Constr.constr_pattern; pri = natural; "["; tac = tactic; "]" -> - VernacHintDestruct (id,dloc,hyptyp,pri,tac) + VernacHintDestruct (local,id,dloc,hyptyp,pri,tac) | IDENT "Hint"; local = locality; hintname = base_ident; dbnames = opt_hintbases; ":="; h = hint -> - VernacHints (dbnames, h hintname) + VernacHints (local,dbnames, h hintname) | IDENT "Hints"; local = locality; (dbnames,h) = hints -> - VernacHints (dbnames, h) + VernacHints (local,dbnames, h) (*This entry is not commented, only for debug*) @@ -106,6 +106,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] |