From 2f521670fbd84a118be56d5397dfeb8bcc404f19 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 Jan 2014 15:57:31 +0100
Subject: Removing the [Require "file"] syntax.

---
 toplevel/vernac_classifier.ml | 1 -
 toplevel/vernacentries.ml     | 4 ----
 2 files changed, 5 deletions(-)

(limited to 'toplevel')

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
-- 
cgit v1.2.3