diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 8 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 5 |
2 files changed, 6 insertions, 7 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index acfbaa14f..b99cc02a3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -599,7 +599,7 @@ let vernac_end_segment (_,id as lid) = (* Libraries *) -let vernac_require import _ qidl = +let vernac_require import qidl = let qidl = List.map qualid_of_reference qidl in let modrefl = Flags.silently (List.map Library.try_locate_qualified_library) qidl in if Dumpglob.dump () then @@ -686,7 +686,7 @@ let vernac_set_used_variables l = (*****************************) (* Auxiliary file management *) -let vernac_require_from export spec filename = +let vernac_require_from export filename = Library.require_library_from_file None (System.expand_path_macros filename) export @@ -1463,7 +1463,7 @@ let interp c = match c with | VernacEndSegment lid -> vernac_end_segment lid - | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl + | VernacRequire (export, qidl) -> vernac_require export qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid | VernacCoercion (str,r,s,t) -> vernac_coercion str r s t @@ -1481,7 +1481,7 @@ let interp c = match c with | VernacSolveExistential (n,c) -> vernac_solve_existential n c (* Auxiliary file and library management *) - | VernacRequireFrom (exp,spec,f) -> vernac_require_from exp spec f + | 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 diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 850bc111a..6566fe59c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -128,7 +128,6 @@ type locality_flag = bool (* true = Local; false = Global *) type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) -type specif_flag = bool (* true = Specification; false = Implementation *) type inductive_flag = Decl_kinds.recursivity_kind type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type infer_flag = bool (* true = try to Infer record; false = nothing *) @@ -249,7 +248,7 @@ type vernac_expr = | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of - export_flag option * specif_flag option * lreference list + export_flag option * lreference list | VernacImport of export_flag * lreference list | VernacCanonical of reference or_by_notation | VernacCoercion of locality * reference or_by_notation * @@ -288,7 +287,7 @@ type vernac_expr = | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) - | VernacRequireFrom of export_flag option * specif_flag option * string + | VernacRequireFrom of export_flag option * string | VernacAddLoadPath of rec_flag * string * dir_path option | VernacRemoveLoadPath of string | VernacAddMLPath of rec_flag * string |