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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/interface/xlate.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index d294af68d..b4e0e69bb 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -1632,7 +1632,7 @@ let rec xlate_module_expr = function let rec xlate_vernac = function - | VernacDeclareTacticDefinition (true, tacs) -> + | VernacDeclareTacticDefinition (false, true, tacs) -> (match List.map (function (id, _, body) -> @@ -1642,8 +1642,10 @@ let rec xlate_vernac = | fst::tacs1 -> CT_tactic_definition (CT_tac_def_ne_list(fst, tacs1))) - | VernacDeclareTacticDefinition(false, _) -> - xlate_error "obsolete tactic definition not handled" + | VernacDeclareTacticDefinition(_, false, _) -> + xlate_error "obsolete tactic definition not handled" + | VernacDeclareTacticDefinition(true, _, _) -> + xlate_error "TODO: Local keyword" | VernacLoad (verbose,s) -> CT_load ( (match verbose with |