Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg

3 files changed, 21 insertions, 21 deletions

diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index cd9d3669..b6af3abc 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_makefile.ml4 8840 2006-05-22 13:51:14Z notin $ *)
+(* $Id: coq_makefile.ml4 10185 2007-10-06 18:05:13Z herbelin $ *)
 
 (* créer un Makefile pour un développement Coq automatiquement *)
 
@@ -175,8 +175,8 @@ let variables l =
     | _ :: r -> var_aux r
   in
   section "Variables definitions.";
-  print "CAMLP4LIB=`camlp4 -where`\n";
-(*  print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *)
+  print "CAMLP4LIB=`camlp5 -where 2> /dev/null || camlp4 -where`\n";
+  print "CAMLP4=`basename $CAMLP4LIB`\n"; 
   print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
   -I $(COQTOP)/library -I $(COQTOP)/parsing \\
   -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
@@ -204,8 +204,8 @@ let variables l =
   print "CAMLOPTLINK=ocamlopt\n";
   print "COQDEP=$(COQBIN)coqdep -c\n";
   print "GRAMMARS=grammar.cma\n";
-  print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n";
-  print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
+  print "CAMLP4EXTEND=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
+  print "PP=-pp \"$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
   var_aux l;
   print "\n"
 
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 89f39b22..e787cdb3 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep.ml 9808 2007-04-29 07:15:18Z herbelin $ *)
+(* $Id: coqdep.ml 10196 2007-10-08 13:50:39Z notin $ *)
 
 open Printf
 open Coqdep_lexer
@@ -108,12 +108,12 @@ let absolute_dir dir =
 
 let absolute_file_name basename odir =
   let dir = match odir with Some dir -> dir | None -> "." in
-  absolute_dir dir / basename
+  absolute_dir dir // basename
      
 let file_name = function
   | (s,None)     -> file_concat s 
   | (s,Some ".") -> file_concat s
-  | (s,Some d)   -> d / file_concat s
+  | (s,Some d)   -> d // file_concat s
 
 let traite_fichier_ML md ext =
   try 
@@ -165,7 +165,7 @@ let cut_prefix p s =
   if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s
 
 let canonize f =
-  let f' = absolute_dir (Filename.dirname f) / Filename.basename f in
+  let f' = absolute_dir (Filename.dirname f) // Filename.basename f in
   match List.filter (fun (_,full) -> f' = full) !vAccu with
     | (f,_) :: _ -> f
     | _ -> f
@@ -411,7 +411,7 @@ let all_subdirs root_dir log_dir =
 	let f = readdir dirh in
 	if f <> "." && f <> ".." then
 	  let file = dir@[f] in
-          let filename = phys_dir/f in
+          let filename = phys_dir//f in
 	  if (stat filename).st_kind = S_DIR then begin
 	    add (filename,file);
 	    traverse filename file
@@ -429,7 +429,7 @@ let usage () =
   exit 1
 
 let add_coqlib_known dir_name f =
-  let complete_name = dir_name/f in
+  let complete_name = dir_name//f in
   let lib_name = Filename.basename dir_name in
   match try (stat complete_name).st_kind with _ -> S_BLK with 
     | S_REG -> 
@@ -458,7 +458,7 @@ let coqdep () =
       match (old_dirname,new_dirname) with 
 	| (d, ".") -> d
 	| (None,d) -> Some d
-	| (Some d1,d2) -> Some (d1/d2) 
+	| (Some d1,d2) -> Some (d1//d2) 
     in
     let complete_name = file_name ([name],dirname) in
     match try (stat complete_name).st_kind with _ -> S_BLK with 
@@ -468,7 +468,7 @@ let coqdep () =
              let newdirname = 
                match dirname with 
                  | None -> name
-                 | Some d -> d/name 
+                 | Some d -> d//name 
 	     in
 	     try 
 	       while true do treat (Some newdirname) (readdir dir) done
@@ -490,7 +490,7 @@ let coqdep () =
       | _ -> ()
   in 
   let add_known phys_dir log_dir f =
-    let complete_name = phys_dir/f in
+    let complete_name = phys_dir//f in
     match try (stat complete_name).st_kind with _ -> S_BLK with 
 	| S_REG ->
 	    if Filename.check_suffix f ".ml" then
@@ -505,7 +505,7 @@ let coqdep () =
 	    else if Filename.check_suffix f ".v" then
 	      let basename = Filename.chop_suffix f ".v" in
               let name = log_dir@[basename] in
-              let file = phys_dir/basename in
+              let file = phys_dir//basename in
               let paths = [name;[basename]] in
 	      List.iter
                 (fun n -> safe_addQueue clash_v vKnown (n,file)) paths
@@ -546,11 +546,11 @@ let coqdep () =
   parse (List.tl (Array.to_list Sys.argv));
   List.iter
     (fun (s,_) -> add_coqlib_directory s)
-    (all_subdirs (!coqlib/"theories") "Coq");
+    (all_subdirs (!coqlib//"theories") "Coq");
   List.iter 
     (fun (s,_) -> add_coqlib_directory s)
-    (all_subdirs (!coqlib/"contrib") "Coq");
-  add_coqlib_directory (!coqlib/"user-contrib");
+    (all_subdirs (!coqlib//"contrib") "Coq");
+  add_coqlib_directory (!coqlib//"user-contrib");
   mliKnown := !mliKnown @ (List.map (fun (f,_,d) -> (f,d)) !mliAccu);
   mlKnown  := !mlKnown @ (List.map (fun (f,_,d) -> (f,d)) !mlAccu);
   warning_mult ".mli" !mliKnown;
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index c63a6a9b..2bf615d3 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 10017 2007-07-18 13:23:55Z notin $ i*)
+(*i $Id: pretty.mll 10074 2007-08-13 12:19:44Z notin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -367,7 +367,7 @@ rule coq_bol = parse
 	coq_bol lexbuf }
   | space* "(*"
       { let eol = comment lexbuf in
-	  if eol then coq_bol lexbuf else coq lexbuf }
+	  if eol then begin line_break(); coq_bol lexbuf end else coq lexbuf }
   | eof 
       { () }
   | _
@@ -578,7 +578,7 @@ and body = parse
   | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true }      
   | '.' space+ { char '.'; char ' '; false }
   | "(*" { let eol = comment lexbuf in 
-	     if eol then body_bol lexbuf else body lexbuf }
+	     if eol then begin line_break(); body_bol lexbuf end else body lexbuf }
   | identifier 
       { let s = lexeme lexbuf in 
 	  ident s (lexeme_start lexbuf);