Correction du bug #1814 (trunk et v8.1) + améliorations dans coqdep et coq_makefile

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

4 files changed, 101 insertions, 106 deletions

diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index d641f8744..0599c4982 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -145,25 +145,9 @@ let implicit () =
     print "%.g.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html -g $< -o $@\n\n";
     print "%.v.d: %.v\n";
     print "\t$(COQDEP) -glob -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
-
-  and ml_suffixes =
-    if !some_mlfile then 
-      [ ".mli"; ".ml"; ".cmo"; ".cmi"; ".cmx" ]
-    else 
-      []
-  and v_suffixes =
-    if !some_vfile then 
-      [ ".v"; ".vo"; ".vi"; ".g"; ".html"; ".tex"; ".g.tex"; ".g.html" ] 
-    else 
-      []
   in
-  let suffixes = ml_suffixes @ v_suffixes in
-  if suffixes <> [] then begin
-    print ".SUFFIXES: "; print_list " " suffixes;
-    print "\n\n"
-  end;
-  if !some_mlfile then ml_rules ();
-  if !some_vfile then v_rule ()
+    if !some_mlfile then ml_rules ();
+    if !some_vfile then v_rule ()
 
 let variables l =
   let rec var_aux = function
@@ -171,10 +155,10 @@ let variables l =
     | Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r
     | _ :: r -> var_aux r
   in
-  section "Variables definitions.";
-  print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n";
-  print "CAMLP4:=$(notdir $(CAMLP4LIB))\n"; 
-  print "COQSRC:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
+    section "Variables definitions.";
+    print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n";
+    print "CAMLP4:=$(notdir $(CAMLP4LIB))\n"; 
+    print "COQSRC:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
   -I $(COQTOP)/library -I $(COQTOP)/parsing \\
   -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
   -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\
@@ -185,28 +169,28 @@ let variables l =
   -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \\
   -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \\
   -I $(CAMLP4LIB)\n";
-  print "ZFLAGS:=$(OCAMLLIBS) $(COQSRC)\n";
-  if !opt = "-byte" then 
-    print "override OPT:=-byte\n"
-  else
-    print "OPT:=\n";
-  if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n";
-  (* Coq executables and relative variables *)
-  print "COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
-  print "COQC:=$(COQBIN)coqc\n";
-  print "COQDEP:=$(COQBIN)coqdep -c\n";
-  print "GALLINA:=$(COQBIN)gallina\n";
-  print "COQDOC:=$(COQBIN)coqdoc\n";
-  (* Caml executables and relative variables *)
-  printf "CAMLC:=$(CAMLBIN)ocamlc -rectypes -c\n";
-  printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -c\n";
-  printf "CAMLLINK:=$(CAMLBIN)ocamlc\n";
-  printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt\n";
-  print "GRAMMARS:=grammar.cma\n";
-  print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
-  print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
-  var_aux l;
-  print "\n"
+    print "ZFLAGS:=$(OCAMLLIBS) $(COQSRC)\n";
+    if !opt = "-byte" then 
+      print "override OPT:=-byte\n"
+    else
+      print "OPT:=\n";
+    if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n";
+    (* Coq executables and relative variables *)
+    print "COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
+    print "COQC:=$(COQBIN)coqc\n";
+    print "COQDEP:=$(COQBIN)coqdep -c\n";
+    print "GALLINA:=$(COQBIN)gallina\n";
+    print "COQDOC:=$(COQBIN)coqdoc\n";
+    (* Caml executables and relative variables *)
+    printf "CAMLC:=$(CAMLBIN)ocamlc -rectypes -c\n";
+    printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -c\n";
+    printf "CAMLLINK:=$(CAMLBIN)ocamlc\n";
+    printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt\n";
+    print "GRAMMARS:=grammar.cma\n";
+    print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
+    print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
+    var_aux l;
+    print "\n"
 
 let absolute_dir dir =
   let current = Sys.getcwd () in
@@ -239,9 +223,10 @@ let include_dirs l =
   in
   let l' = if List.exists (is_included ".") l then l else Include "." :: l in
   let inc_i, inc_r = parse_includes l' in
+  let inc_i' = List.filter (fun d -> List.exists (fun d' -> is_prefix d' d) inc_r) inc_i in 
     section "Libraries definition.";
     print "OCAMLLIBS:="; print_list "\\\n  " inc_i; print "\n";
-    print "COQLIBS:="; print_list "\\\n  " inc_i; print " "; print_list "\\\n  " inc_r; print "\n";
+    print "COQLIBS:="; print_list "\\\n  " inc_i'; print " "; print_list "\\\n  " inc_r; print "\n";
     print "COQDOCLIBS:=";   print_list "\\\n  " inc_r; print "\n\n"
 
 let rec special = function
@@ -281,9 +266,9 @@ let all_target l =
   let rec parse_arguments l = 
     match l with
       | ML n :: r -> let v,m,o = parse_arguments r in (v,n::m,o)
-      | Subdir n :: r -> let v,m,o = parse_arguments r in (n::v,m,o)
+      | Subdir n :: r -> let v,m,o = parse_arguments r in (v,m,n::o)
       | V n :: r -> let v,m,o = parse_arguments r in (n::v,m,o)
-      | Special (n,_,_) :: r -> let v,m,o = (parse_arguments r) in (v,m,n::o)
+      | Special (n,_,_) :: r -> let v,m,o = parse_arguments r in (v,m,n::o)
       | Include _ :: r -> parse_arguments r
       | RInclude _ :: r -> parse_arguments r
       | Def _ :: r -> parse_arguments r
@@ -293,19 +278,27 @@ let all_target l =
       vfiles, mlfiles, other_targets = parse_arguments l
   in
     section "Definition of the \"all\" target.";
-    print "VFILES:="; print_list "\\\n  " vfiles; print "\n";
-    print "VOFILES:=$(VFILES:.v=.vo)\n";
-    print "GLOBFILES:=$(VFILES:.v=.glob)\n";
-    print "VIFILES:=$(VFILES:.v=.vi)\n";
-    print "GFILES:=$(VFILES:.v=.g)\n";
-    print "HTMLFILES:=$(VFILES:.v=.html)\n";
-    print "GHTMLFILES:=$(VFILES:.v=.g.html)\n";
-    print "MLFILES:="; print_list "\\\n  " mlfiles; print "\n";
-    print "CMOFILES:=$(MLFILES:.ml=.cmo)";
-    print "\n";
-    print "all: $(VOFILES) $(CMOFILES) "; print_list "\\\n  " other_targets;
-    print "\n\n";
-    if !some_vfile then begin
+    if !some_vfile then
+      begin
+	print "VFILES:="; print_list "\\\n  " vfiles; print "\n";
+	print "VOFILES:=$(VFILES:.v=.vo)\n";
+	print "GLOBFILES:=$(VFILES:.v=.glob)\n";
+	print "VIFILES:=$(VFILES:.v=.vi)\n";
+	print "GFILES:=$(VFILES:.v=.g)\n";
+	print "HTMLFILES:=$(VFILES:.v=.html)\n";
+	print "GHTMLFILES:=$(VFILES:.v=.g.html)\n"
+      end;
+    if !some_mlfile then
+      begin
+	print "MLFILES:="; print_list "\\\n  " mlfiles; print "\n";
+	print "CMOFILES:=$(MLFILES:.ml=.cmo)\n";
+      end;
+    print "\nall: ";
+    if !some_vfile then print "$(VOFILES) ";
+    if !some_mlfile then print "$(CMOFILES) ";
+    print_list "\\\n  " other_targets; print "\n";
+    if !some_vfile then 
+      begin
 	print "spec: $(VIFILES)\n\n";
 	print "gallina: $(GFILES)\n\n";
 	print "html: $(GLOBFILES) $(VFILES)\n";
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 097e19fe2..f188ebfa6 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -41,6 +41,11 @@ let file_concat l =
   if l=[] then "<empty>" else
     List.fold_left (//) (List.hd l) (List.tl l)
 
+let make_ml_module_name filename =
+  (* Computes a ML Module name from its physical name *)
+  let basename = Filename.chop_extension filename in
+    String.capitalize basename
+
 (* Files specified on the command line *)
 let mlAccu  = ref ([] : (string * string * dir) list) 
 and mliAccu = ref ([] : (string * string * dir) list) 
@@ -234,12 +239,13 @@ let traite_fichier_Coq verbose f =
 	  | Declare sl -> 
 	      List.iter 
 		(fun str ->
-		   if not (List.mem str !deja_vu_ml) then begin
-		     addQueue deja_vu_ml str;
-               	     try
-              	       let mldir = Hashtbl.find mlKnown str in
-              	       printf " %s.cmo" (file_name ([String.uncapitalize str],mldir))
-              	     with Not_found -> ()
+		  let s = String.capitalize str in
+		    if not (List.mem s !deja_vu_ml) then begin
+			addQueue deja_vu_ml s;
+               	       try
+              		 let mldir = Hashtbl.find mlKnown s in
+              		   printf " %s.cmo" (file_name ([String.uncapitalize s],mldir))
+              	       with Not_found -> ()
 		     end)
 		sl
 	  | Load str -> 
@@ -304,36 +310,37 @@ let traite_Declare f =
   let decl_list = ref ([] : string list) in
   let rec treat = function
     | s :: ll -> 
-	if (Hashtbl.mem mlKnown s) & not (List.mem s !decl_list) then begin
-       	  let mldir = Hashtbl.find mlKnown s in
-	  let fullname = file_name ([(String.uncapitalize s)],mldir) in
-	  let depl = mL_dep_list s (fullname ^ ".ml") in
-	  treat depl;
-	  decl_list := s :: !decl_list
-	end;
-	treat ll
+	let s' = String.capitalize s in
+	  if (Hashtbl.mem mlKnown s') & not (List.mem s' !decl_list) then begin
+       	      let mldir = Hashtbl.find mlKnown s in
+	      let fullname = file_name ([(String.uncapitalize s')],mldir) in
+	      let depl = mL_dep_list s (fullname ^ ".ml") in
+		treat depl;
+		decl_list := s :: !decl_list
+	    end;
+	  treat ll
     | [] -> ()
   in
-  try
-    let chan = open_in f in
-    let buf = Lexing.from_channel chan in
-    begin try 
-      while true do
-      	let tok = coq_action buf in
-      	(match tok with
-	   | Declare sl -> 
-	       decl_list := [];
-	       treat sl;
-	       decl_list := List.rev !decl_list;
-	       if !option_D then 
-		 affiche_Declare f !decl_list
-	       else if !decl_list <> sl then
-		 warning_Declare f !decl_list
-	   | _ -> ())
-      done
-    with Fin_fichier -> () end;
-    close_in chan
-  with Sys_error _ -> ()
+    try
+      let chan = open_in f in
+      let buf = Lexing.from_channel chan in
+	begin try 
+	    while true do
+      	      let tok = coq_action buf in
+      		(match tok with
+		  | Declare sl -> 
+		      decl_list := [];
+		      treat sl;
+		      decl_list := List.rev !decl_list;
+		      if !option_D then 
+			affiche_Declare f !decl_list
+		      else if !decl_list <> sl then
+			warning_Declare f !decl_list
+		  | _ -> ())
+	    done
+	  with Fin_fichier -> () end;
+	close_in chan
+    with Sys_error _ -> ()
 
 let file_mem (f,_,d) =
   let rec loop = function
@@ -407,11 +414,6 @@ let usage () =
   flush stderr;
   exit 1
 
-let make_ml_module_name filename =
-  (* Computes a ML Module name from its physical name *)
-  let basename = Filename.chop_extension filename in
-    String.capitalize basename
-
 let add_coqlib_known phys_dir log_dir f = 
   if Filename.check_suffix f ".vo" then
     let basename = Filename.chop_suffix f ".vo" in
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index ffb35c528..32ad4bdc5 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -215,7 +215,7 @@ and modules = parse
   | '"' [^'"']* '"'
         { let lex = (Lexing.lexeme lexbuf) in 
 	  let str = String.sub lex 1 (String.length lex - 2) in
-	  mllist := str :: !mllist; modules lexbuf }
+	    mllist := str :: !mllist; modules lexbuf}
   | _   { (Declare (List.rev !mllist)) }   
 
 and qual_id = parse
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index db1caaeee..8774d9d2e 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -189,7 +189,7 @@ let symbolchar_no_brackets =
   '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
 let symbolchar = symbolchar_no_brackets | '[' | ']'
 let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
-
+let printing_token = (token | id)+
 
 let thm_token = 
   "Theorem" 
@@ -370,9 +370,9 @@ rule coq_bol = parse
 	    let eol= body lexbuf in
 	      if eol then coq_bol lexbuf else coq lexbuf }
 
-  | space* "(**" space+ "printing" space+ (identifier | token) space+
+  | space* "(**" space+ "printing" space+ printing_token space+
       { let tok = lexeme lexbuf in
-	let s = printing_token lexbuf in
+	let s = printing_token_body lexbuf in
 	  add_printing_token tok s;
 	  coq_bol lexbuf }
   | space* "(**" space+ "printing" space+
@@ -617,7 +617,7 @@ and body = parse
       { let s = lexeme lexbuf in 
 	  Output.ident s (lexeme_start lexbuf); 
 	  body lexbuf }
-  | token
+  | printing_token
       { let s = lexeme lexbuf in
 	  Output.symbol s; body lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
@@ -645,13 +645,13 @@ and skip_hide = parse
 
 (*s Reading token pretty-print *)
 
-and printing_token = parse
+and printing_token_body = parse
   | "*)" | eof 
 	{ let s = Buffer.contents token_buffer in 
 	  Buffer.clear token_buffer;
 	  s }
   | _   { Buffer.add_string token_buffer (lexeme lexbuf); 
-	  printing_token lexbuf }
+	  printing_token_body lexbuf }
 
 (*s Applying the scanners to files *)