diff options
Diffstat (limited to 'plugins/interface')
| -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 d294af68d2..b4e0e69bbf 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 |