From 8b4637c2a5ff1b6774be4f40665ccc03b687a47e Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 25 Oct 2006 13:00:22 +0000
Subject: coqdep -slash

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9276 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 man/coqdep.1 | 33 ++++++++++++++++++++++-----------
 1 file changed, 22 insertions(+), 11 deletions(-)

(limited to 'man/coqdep.1')

diff --git a/man/coqdep.1 b/man/coqdep.1
index 01d080fc2..6ae89f8bd 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -23,6 +23,9 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs
 [
 .BI \-D
 ]
+[
+.BI \-slash
+]
 .I filename ...
 .I directory ...
 
@@ -37,10 +40,11 @@ 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),
-and
 .IR Declare \& 
 .IR ML \& 
 .IR Module \&
+commands and
+.IR Load \&
 commands. Dependencies relative to modules from the Coq library are not
 printed.
 
@@ -54,8 +58,7 @@ directives and the dot notation
 .TP
 .BI \-c
 Prints the dependencies of Caml modules.
-(On Caml modules, the behaviour is exactly the same as cldepend,
-except that nested comments and strings are correctly handled).
+(On Caml modules, the behaviour is exactly the same as ocamldep).
 .TP
 .BI \-w
 Prints a warning if a Coq command
@@ -78,6 +81,10 @@ of each Coq file given as argument and complete (if needed)
 the list of Caml modules. The new command is printed on
 the standard output. No dependency is computed with this option.
 .TP 
+.BI \-slash
+Prints paths using a slash instead of the OS specific separator. This
+option is useful when developping under Cygwin.
+.TP
 .BI \-I \ directory
 The files .v .ml .mli of the directory
 .IR directory \&
@@ -87,7 +94,7 @@ but their own dependencies are not printed.
 .BI \-coqlib \ directory
 Indicates where is the Coq library. The default value has been
 determined at installation time, and therefore this option should not
-be used.
+be used under normal circumstances.
 
 
 .SH SEE ALSO
@@ -120,7 +127,7 @@ Consider the files (in the same directory):
 where
 .TP
 .BI \+ 
-D.ml contains the commands `#open "A"', `#open "B"' and `type t = C__t' ;
+D.ml contains the commands `open A', `open B' and `type t = C.t' ;
 .TP
 .BI \+
 Y.v contains the command `Require X' ;
@@ -135,7 +142,7 @@ example% coqdep -I . *.v
 .RS
 .sp .5
 .nf
-.B Z.vo: Z.v ./X.vo ./D.zo
+.B Z.vo: Z.v ./X.vo ./D.cmo
 .B Y.vo: Y.v ./X.vo
 .B X.vo: X.v
 .fi
@@ -150,7 +157,7 @@ example% coqdep -w -I . *.v
 .RS
 .sp .5
 .nf
-.B Z.vo: Z.v ./X.vo ./D.zo
+.B Z.vo: Z.v ./X.vo ./D.cmo
 .B Y.vo: Y.v ./X.vo
 .B X.vo: X.v
 ### Warning : In file Z.v, the ML modules declaration should be
@@ -167,10 +174,14 @@ example% coqdep -c -I . *.ml
 .RS
 .sp .5
 .nf
-.B D.zo: D.ml ./A.zo ./B.zo ./C.zo
-.B C.zo: C.ml
-.B B.zo: B.ml
-.B A.zo: A.ml
+.B D.cmo: D.ml ./A.cmo ./B.cmo ./C.cmo
+.B D.cmx: D.ml ./A.cmx ./B.cmx ./C.cmx
+.B C.cmo: C.ml
+.B C.cmx: C.ml
+.B B.cmo: B.ml
+.B B.cmx: B.ml
+.B A.cmo: A.ml
+.B A.cmx: A.ml
 .fi
 .RE
 .br
-- 
cgit v1.2.3