diff options
| author | Pierre-Marie Pédrot | 2016-03-20 02:23:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 02:41:58 +0100 |
| commit | 4f52bd681ad9bbcbbd68406a58b47d8e962336ed (patch) | |
| tree | 5b891de8b42d9cb20ec3273ae1e02bd586f42fd0 /parsing | |
| parent | 9f5d9cd2622f3890e70dad01898868fe29df6048 (diff) | |
Moving the Ltac definition command to an EXTEND based command.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 3 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
3 files changed, 1 insertions, 9 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0ad39d8047..8d7b6a2b48 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -751,11 +751,7 @@ GEXTEND Gram GLOBAL: command query_command class_rawexpr; command: - [ [ IDENT "Ltac"; - l = LIST1 tacdef_body SEP "with" -> - VernacDeclareTacticDefinition l - - | IDENT "Comments"; l = LIST0 comment -> VernacComments l + [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 9c2f09db84..c7cb62d592 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -364,9 +364,6 @@ module Tactic = (* Main entry for quotations *) let tactic_eoi = eoi_entry tactic - (* For Ltac definition *) - let tacdef_body = Gram.entry_create "tactic:tacdef_body" - end module Vernac_ = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7410d4e44c..35973a4d72 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -229,7 +229,6 @@ 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 : Vernacexpr.tacdef_body Gram.entry end module Vernac_ : |