diff options
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 |