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