diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac_classifier.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
2 files changed, 0 insertions, 5 deletions
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index e6bb80be0e..49cbcd246b 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 206a565f14..ae6ca4d388 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 |