From 4767d724d489a7ad67f696e9401e70b9f9ae2143 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 15 Oct 2007 19:55:12 +0000 Subject: Imported Upstream version 8.1.pl2+dfsg --- tools/coq_makefile.ml4 | 10 +++++----- tools/coqdep.ml | 26 +++++++++++++------------- tools/coqdoc/pretty.mll | 6 +++--- 3 files changed, 21 insertions(+), 21 deletions(-) (limited to 'tools') 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); -- cgit v1.2.3