diff options
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 6 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac_classifier.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
6 files changed, 0 insertions, 16 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 8f959183c..dc2e454f6 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -620,12 +620,6 @@ with the mapping used to compile the file. given, it also imports {\qualid}$_1$, \ldots, {\qualid}$_n$ and all the recursive dependencies that were marked or transitively marked as {\tt Export}. - -\item {\tt Require \zeroone{Import {\sl |} Export} {\str}.} - - This shortcuts the resolution of the qualified name into a library - file name by directly requiring the module to be found in file - {\str}.vo. \end{Variants} \begin{ErrMsgs} 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 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 diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 6ea34185f..2628f732b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -786,8 +786,6 @@ let rec pr_vernac = function str"Existential " ++ int i ++ pr_lconstrarg c (* Auxiliary file and library management *) - | VernacRequireFrom (exp, f) -> hov 2 - (str "Require" ++ spc() ++ pr_require_token exp ++ qs f) | VernacAddLoadPath (fl,s,d) -> hov 2 (str"Add" ++ (if fl then str" Rec " else spc()) ++ diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index e6bb80be0..49cbcd246 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -166,7 +166,6 @@ let rec classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) | VernacProofMode _ - | VernacRequireFrom _ -> VtSideff [], VtNow (* These are ambiguous *) | VernacInstance _ -> VtUnknown, VtNow (* Stm will install a new classifier to handle these *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 206a565f1..ae6ca4d38 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -815,9 +815,6 @@ let vernac_set_used_variables e = let expand filename = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename -let vernac_require_from export filename = - Library.require_library_from_file None (expand filename) export - let vernac_add_loadpath isrec pdir ldiropt = let pdir = expand pdir in let alias = Option.default Nameops.default_root_prefix ldiropt in @@ -1684,7 +1681,6 @@ let interp ?proof locality c = | VernacSolveExistential (n,c) -> vernac_solve_existential n c (* Auxiliary file and library management *) - | VernacRequireFrom (exp, f) -> vernac_require_from exp f | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias | VernacRemoveLoadPath s -> vernac_remove_loadpath s | VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s |