aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/RefMan-uti.tex2
-rw-r--r--man/coqdep.15
-rw-r--r--tools/coqdep.ml24
-rwxr-xr-xtools/coqdep_lexer.mll22
4 files changed, 17 insertions, 36 deletions
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 2305fa431..f1dde04ad 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -64,7 +64,7 @@ argument, it is recursively looked at.
Dependencies of \Coq\ modules are computed by looking at {\tt Require}
commands ({\tt Require}, {\tt Requi\-re Export}, {\tt Require Import},
-{\tt Require Implementation}), but also at the command {\tt Declare ML Module}.
+but also at the command {\tt Declare ML Module}.
Dependencies of \ocaml\ modules are computed by looking at
\verb!open! commands and the dot notation {\em module.value}. However,
diff --git a/man/coqdep.1 b/man/coqdep.1
index e2cbb40e0..e9e0dd3e3 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -39,7 +39,7 @@ When a directory is given as argument, it is recursively looked at.
Dependencies of Coq modules are computed by looking at
.IR Require \&
-commands (Require, Require Export, Require Import, Require Implementation),
+commands (Require, Require Export, Require Import),
.IR Declare \&
.IR ML \&
.IR Module \&
@@ -69,9 +69,6 @@ is incorrect. (For instance, you wrote `Declare ML Module "A".',
but the module A contains #open "B"). The correct command is printed
(see option \-D). The warning is printed on standard error.
.TP
-.BI \-i
-Prints also the dependencies for .vi files (Coq specification modules).
-.TP
.BI \-D
This commands looks for every command
.IR Declare \&
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 393554568..019ee6b1a 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -18,13 +18,11 @@ let stdout = Pervasives.stdout
let option_c = ref false
let option_D = ref false
let option_w = ref false
-let option_i = ref false
let option_sort = ref false
let option_noglob = ref false
let option_slash = ref false
let suffixe = ref ".vo"
-let suffixe_spec = ref ".vi"
type dir = string option
@@ -184,13 +182,13 @@ let sort () =
try
while true do
match coq_action lb with
- | Require (_, sl) ->
+ | Require sl ->
List.iter
(fun s ->
try loop (Hashtbl.find vKnown s)
with Not_found -> ())
sl
- | RequireString (_, s) -> loop s
+ | RequireString s -> loop s
| _ -> ()
done
with Fin_fichier ->
@@ -210,26 +208,24 @@ let traite_fichier_Coq verbose f =
while true do
let tok = coq_action buf in
match tok with
- | Require (spec,strl) ->
+ | Require strl ->
List.iter (fun str ->
if not (List.mem str !deja_vu_v) then begin
addQueue deja_vu_v str;
try
let file_str = safe_assoc verbose f str in
- printf " %s%s" (canonize file_str)
- (if spec then !suffixe_spec else !suffixe)
+ printf " %s%s" (canonize file_str) !suffixe
with Not_found ->
if verbose && not (Hashtbl.mem coqlibKnown str) then
warning_module_notfound f str
end) strl
- | RequireString (spec,s) ->
+ | RequireString s ->
let str = Filename.basename s in
if not (List.mem [str] !deja_vu_v) then begin
addQueue deja_vu_v [str];
try
let file_str = Hashtbl.find vKnown [str] in
- printf " %s%s" (canonize file_str)
- (if spec then !suffixe_spec else !suffixe)
+ printf " %s%s" (canonize file_str) !suffixe
with Not_found ->
if not (Hashtbl.mem coqlibKnown [str]) then
warning_notfound f s
@@ -391,11 +387,6 @@ let coq_dependencies () =
printf "%s%s%s: %s.v" name !suffixe glob name;
traite_fichier_Coq true (name ^ ".v");
printf "\n";
- if !option_i then begin
- printf "%s%s%s: %s.v" name !suffixe_spec glob name;
- traite_fichier_Coq false (name ^ ".v");
- printf "\n";
- end;
flush stdout)
(List.rev !vAccu)
@@ -512,7 +503,6 @@ let rec parse = function
| "-c" :: ll -> option_c := true; parse ll
| "-D" :: ll -> option_D := true; parse ll
| "-w" :: ll -> option_w := true; parse ll
- | "-i" :: ll -> option_i := true; parse ll
| "-boot" :: ll -> Flags.boot := true; parse ll
| "-sort" :: ll -> option_sort := true; parse ll
| "-noglob" :: ll | "-no-glob" :: ll -> option_noglob := true; parse ll
@@ -522,7 +512,7 @@ let rec parse = function
| "-R" :: ([] | [_]) -> usage ()
| "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
| "-coqlib" :: [] -> usage ()
- | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll
+ | "-suffix" :: (s :: ll) -> suffixe := s ; parse ll
| "-suffix" :: [] -> usage ()
| "-slash" :: ll -> option_slash := true; parse ll
| f :: ll -> treat_file None f; parse ll
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 32ad4bdc5..67dea5a3c 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -18,8 +18,8 @@
type spec = bool
type coq_token =
- | Require of spec * string list list
- | RequireString of spec * string
+ | Require of string list list
+ | RequireString of string
| Declare of string list
| Load of string
@@ -30,9 +30,7 @@
let module_current_name = ref []
let module_names = ref []
let ml_module_name = ref ""
-
- let specif = ref false
-
+
let mllist = ref ([] : string list)
let field_name s = String.sub s 1 (String.length s - 1)
@@ -49,11 +47,11 @@ let dot = '.' ( space+ | eof)
rule coq_action = parse
| "Require" space+
- { specif := false; module_names := []; opened_file lexbuf }
+ { module_names := []; opened_file lexbuf }
| "Require" space+ "Export" space+
- { specif := false; module_names := []; opened_file lexbuf}
+ { module_names := []; opened_file lexbuf}
| "Require" space+ "Import" space+
- { specif := false; module_names := []; opened_file lexbuf}
+ { module_names := []; opened_file lexbuf}
| "Declare" space+ "ML" space+ "Module" space+
{ mllist := []; modules lexbuf}
| "Load" space+
@@ -169,10 +167,6 @@ and opened_file = parse
| "(*" (* "*)" *) { comment_depth := 1; comment lexbuf; opened_file lexbuf }
| space+
{ opened_file lexbuf }
- | "Implementation"
- { opened_file lexbuf }
- | "Specification"
- { specif := true; opened_file lexbuf }
| coq_ident
{ module_current_name := [Lexing.lexeme lexbuf];
opened_file_fields lexbuf }
@@ -184,7 +178,7 @@ and opened_file = parse
if Filename.check_suffix str ".v" then
Filename.chop_suffix str ".v"
else str in
- RequireString (!specif, str) }
+ RequireString str }
| eof { raise Fin_fichier }
| _ { opened_file lexbuf }
@@ -204,7 +198,7 @@ and opened_file_fields = parse
opened_file_fields lexbuf }
| dot { module_names :=
List.rev !module_current_name :: !module_names;
- Require (!specif, List.rev !module_names) }
+ Require (List.rev !module_names) }
| eof { raise Fin_fichier }
| _ { opened_file_fields lexbuf }
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 12:44:42 +0000