diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-07 18:02:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 15:52:56 +0200 |
| commit | dfac5aa2285de5b89f08ada3c30c0a1594737440 (patch) | |
| tree | 37fa3f3481d03c4a777595e1ec0eab631cd528aa /ltac/g_ltac.ml4 | |
| parent | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (diff) | |
Making Vernacexpr independent from Tacexpr.
Diffstat (limited to 'ltac/g_ltac.ml4')
| -rw-r--r-- | ltac/g_ltac.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index c67af33e2..42276ad3f 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -287,15 +287,15 @@ GEXTEND Gram (* Definitions for tactics *) tacdef_body: [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> - if redef then Vernacexpr.TacticRedefinition (name, TacFun (it, body)) + if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in - Vernacexpr.TacticDefinition (id, TacFun (it, body)) + Tacexpr.TacticDefinition (id, TacFun (it, body)) | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> - if redef then Vernacexpr.TacticRedefinition (name, body) + if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in - Vernacexpr.TacticDefinition (id, body) + Tacexpr.TacticDefinition (id, body) ] ] ; tactic: |