diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-09 15:38:20 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-09 15:38:20 +0200 |
| commit | 81753dcda29bf7d7ecd6c8c0ddb3347f4cd49766 (patch) | |
| tree | 8af2a8e24a87fb5dea0bb6dc2feadd6b0e06fd3b /parsing | |
| parent | d5534aab708e5d3bd6c3633dc9d028016eeb3076 (diff) | |
| parent | 347d94a4b966d0cc4a3a04814b0c76c4b05caa11 (diff) | |
Merge PR #1114: Generic handling of nameable objects for plugins
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 819d236cd..3e0b85b54 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1020,8 +1020,7 @@ GEXTEND Gram | IDENT "Term"; qid = smart_global -> LocateTerm qid | IDENT "File"; f = ne_string -> LocateFile f | IDENT "Library"; qid = global -> LocateLibrary qid - | IDENT "Module"; qid = global -> LocateModule qid - | IDENT "Ltac"; qid = global -> LocateTactic qid ] ] + | IDENT "Module"; qid = global -> LocateModule qid ] ] ; option_value: [ [ n = integer -> IntValue (Some n) |