diff options
Diffstat (limited to 'parsing/g_ltac.ml4')
| -rw-r--r-- | parsing/g_ltac.ml4 | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 959b0e89f..12d53030d 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -29,6 +29,12 @@ let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat +let reference_to_id = function + | Libnames.Ident (loc, id) -> (loc, id) + | Libnames.Qualid (loc,_) -> + Errors.user_err_loc (loc, "", + str "This expression should be a simple identifier.") + (* Tactics grammar rules *) GEXTEND Gram @@ -250,9 +256,16 @@ GEXTEND Gram (* Definitions for tactics *) tacdef_body: [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> - (name, redef, TacFun (it, body)) + if redef then Vernacexpr.TacticRedefinition (name, TacFun (it, body)) + else + let id = reference_to_id name in + Vernacexpr.TacticDefinition (id, TacFun (it, body)) | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> - (name, redef, body) ] ] + if redef then Vernacexpr.TacticRedefinition (name, body) + else + let id = reference_to_id name in + Vernacexpr.TacticDefinition (id, body) + ] ] ; tactic: [ [ tac = tactic_expr -> tac ] ] |