diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-17 20:58:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-17 20:58:21 +0000 |
| commit | e927e0e71daa736a99518d487e85e7e54ad8edf2 (patch) | |
| tree | e288df03d34556bfd9b766bc70a34b4611eb58aa | |
| parent | 8eb1c255f301500a2981688d57c79f53d8b6acea (diff) | |
Ajout option Local aux Hint
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4175 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 8cd36df1e..82896099f 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] |