diff options
| author | Matej Kosik | 2015-12-16 15:50:40 +0100 |
|---|---|---|
| committer | Matej Kosik | 2015-12-18 15:58:43 +0100 |
| commit | 20641795624dbb03da0401e4dc503660e5e73df6 (patch) | |
| tree | 3e4a94692a2c7ec1c722e8a8a3db94783a4cd684 /parsing | |
| parent | 84f54fd0923c15109910123443348c193e37fe0f (diff) | |
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
The definition of Vernacexpr.VernacDeclareTacticDefinition was changed.
The original definition allowed us to represent non-sensical value such as:
VernacDeclareTacticDefinition(Qualid ..., false, ...)
The new definition prevents that.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 20 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
2 files changed, 11 insertions, 11 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 4a9ca23f15..181c2395d2 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -242,17 +242,17 @@ GEXTEND Gram | n = integer -> MsgInt n ] ] ; - ltac_def_kind: - [ [ ":=" -> false - | "::=" -> true ] ] - ; - (* Definitions for tactics *) - tacdef_body: - [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> - (name, redef, TacFun (it, body)) - | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> - (name, redef, body) ] ] + tacdef_body: + [ [ id = ident; it=LIST1 input_fun; ":="; body = tactic_expr -> + Vernacexpr.TacticDefinition ((!@loc,id), TacFun (it, body)) + | name = Constr.global; it=LIST1 input_fun; "::="; body = tactic_expr -> + Vernacexpr.TacticRedefinition (name, TacFun (it, body)) + | id = ident; ":="; body = tactic_expr -> + Vernacexpr.TacticDefinition ((!@loc,id), body) + | name = Constr.global; "::="; body = tactic_expr -> + Vernacexpr.TacticRedefinition (name, body) + ] ] ; tactic: [ [ tac = tactic_expr -> tac ] ] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ad4d9e5019..fdba413854 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -237,7 +237,7 @@ module Tactic : val binder_tactic : raw_tactic_expr Gram.entry val tactic : raw_tactic_expr Gram.entry val tactic_eoi : raw_tactic_expr Gram.entry - val tacdef_body : (reference * bool * raw_tactic_expr) Gram.entry + val tacdef_body : Vernacexpr.tacdef_body Gram.entry end module Vernac_ : |