Removed a seemingly unused argument in Require of modules, introduced 10 years ago and absent from both coq and contribs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14937 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 11 insertions, 22 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 814ff9a39..029a5c5df 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -409,9 +409,9 @@ GEXTEND Gram
 
       (* Requiring an already compiled module *)
       | IDENT "Require"; export = export_token; qidl = LIST1 global ->
-          VernacRequire (export, None, qidl)
+          VernacRequire (export, qidl)
       | IDENT "Require"; export = export_token; filename = ne_string ->
-	  VernacRequireFrom (export, None, filename)
+	  VernacRequireFrom (export, filename)
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
       | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
       | IDENT "Include"; e = module_expr_inl; l = LIST0 ext_module_expr ->
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c23998613..cff1a5308 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -644,13 +644,8 @@ let rec pr_vernac = function
   (* Gallina extensions *)
   | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
   | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
-  | VernacRequire (exp,spe,l) -> hov 2
+  | VernacRequire (exp, l) -> hov 2
       (str "Require" ++ spc() ++ pr_require_token exp ++
-      (match spe with
-      |	None -> mt()
-      |	Some flag ->
-          (if flag then str"Specification" else str"Implementation") ++
-          spc ()) ++
       prlist_with_sep sep pr_module l)
   | VernacImport (f,l) ->
       (if f then str"Export" else str"Import") ++ spc() ++
@@ -732,13 +727,8 @@ let rec pr_vernac = function
       str"Existential " ++ int i ++ pr_lconstrarg c
 
   (* Auxiliary file and library management *)
-  | VernacRequireFrom (exp,spe,f) -> hov 2
-      (str"Require" ++ spc() ++ pr_require_token exp ++
-      (match spe with
-        | None -> mt()
-        | Some false -> str"Implementation" ++ spc()
-        | Some true -> str"Specification" ++ spc ()) ++
-      qs f)
+  | 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/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