diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-31 15:57:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-02 01:50:28 +0100 |
| commit | 2f521670fbd84a118be56d5397dfeb8bcc404f19 (patch) | |
| tree | a610581a097827b7ad816b4696b9a6a9baf1c066 /parsing | |
| parent | 2ea5251fa8e203d5d5b9a1eb3f6887bafdabe155 (diff) | |
Removing the [Require "file"] syntax.
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 |