diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-14 09:15:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-14 09:15:38 +0000 |
| commit | 3f1769a8002addec9f53969affd6b4cee1ccbbea (patch) | |
| tree | cab9b33832658113f646ebc38d78cd0bb2c83de3 /parsing | |
| parent | 8ddd9ba6efcd32a13b4517a4e80c5fc035a951a8 (diff) | |
Ajout option Local à Hint, Hints et HintDestruct
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
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*) |