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 /intf | |
| parent | 2ea5251fa8e203d5d5b9a1eb3f6887bafdabe155 (diff) | |
Removing the [Require "file"] syntax.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ee51a7694..2df1f1633 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -347,7 +347,6 @@ type vernac_expr = | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) - | VernacRequireFrom of export_flag option * string | VernacAddLoadPath of rec_flag * string * DirPath.t option | VernacRemoveLoadPath of string | VernacAddMLPath of rec_flag * string |