diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-26 14:46:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-26 14:46:43 +0000 |
| commit | a29edb0a5e9d420a3780a7034aad4ef9cfe7c148 (patch) | |
| tree | 9b2ec00ba7d5a91491645c41cc41ab4f2bd07f1a /parsing/g_proofs.ml4 | |
| parent | 5dcc913519b8822ddf59eb3a356028f45f42cc3b (diff) | |
New cleaning phase of the Local/Global option management
- Clarification and documentation of the different styles of
Local/Global modifiers in vernacexpr.ml
- Addition of Global in sections for Open/Close Scope.
- Addition of Local for Ltac when not in sections.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 90245fa45..39e577b88 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -92,16 +92,16 @@ GEXTEND Gram (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; id = IDENT ; b = [ "discriminated" -> true | -> false ] -> - VernacCreateHintDb (use_locality (), id, b) + VernacCreateHintDb (use_module_locality (), id, b) | IDENT "Hint"; local = obsolete_locality; h = hint; dbnames = opt_hintbases -> - VernacHints (enforce_locality_of local,dbnames, h) + VernacHints (enforce_module_locality local,dbnames, h) (* Declare "Resolve" directly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 constr; n = OPT natural; dbnames = opt_hintbases -> - VernacHints (enforce_locality_of false,dbnames, + VernacHints (use_module_locality (),dbnames, HintsResolve (List.map (fun x -> (n, true, x)) lc)) (*This entry is not commented, only for debug*) |