diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 87559c9e6..d5ff2538c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -437,8 +437,6 @@ GEXTEND Gram (* Requiring an already compiled module *) | IDENT "Require"; export = export_token; qidl = LIST1 global -> VernacRequire (export, qidl) - | IDENT "Require"; export = export_token; filename = ne_string -> - VernacRequireFrom (export, filename) | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token ; qidl = LIST1 global -> let qidl = List.map (Libnames.join_reference ns) qidl in |