diff options
| author | notin | 2008-06-24 11:41:12 +0000 |
|---|---|---|
| committer | notin | 2008-06-24 11:41:12 +0000 |
| commit | 4823449f7f3800835bfd5ebc4de5bdf407fdc2c2 (patch) | |
| tree | aea77208ed5b783f4f00c5c6679f1b1bdbbab264 /tools | |
| parent | de45178c0b684a211fa61866e82b045f12f85ffe (diff) | |
Suppression de l'option -dump-glob et ajout d'une option -no-glob
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml4 | 8 | ||||
| -rw-r--r-- | tools/coqdep.ml | 6 |
2 files changed, 7 insertions, 7 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 3138ce4eff..2dfac4e187 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -136,15 +136,15 @@ let implicit () = print "%.ml.d: %.ml\n"; print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) \"$<\" > \"$@\"\n\n" and v_rule () = - print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "%.g: %.v\n\t$(GALLINA) $<\n\n"; print "%.tex: %.v\n\t$(COQDOC) -latex $< -o $@\n\n"; - print "%.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html $< -o $@\n\n"; + print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n"; print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n"; - print "%.g.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html -g $< -o $@\n\n"; + print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n"; print "%.v.d: %.v\n"; - print "\t$(COQDEP) -glob -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" + print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in if !some_mlfile then ml_rules (); if !some_vfile then v_rule () diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 84f9eb3ff7..5a31a64d8c 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -22,7 +22,7 @@ let option_D = ref false let option_w = ref false let option_i = ref false let option_sort = ref false -let option_glob = ref false +let option_noglob = ref false let option_slash = ref false let option_boot = ref false @@ -375,7 +375,7 @@ let mL_dependencies () = let coq_dependencies () = List.iter (fun (name,_) -> - let glob = if !option_glob then " "^name^".glob" else "" in + let glob = if !option_noglob then "" else " "^name^".glob" in printf "%s%s%s: %s.v" name !suffixe glob name; traite_fichier_Coq true (name ^ ".v"); printf "\n"; @@ -503,7 +503,7 @@ let rec parse = function | "-i" :: ll -> option_i := true; parse ll | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll - | "-glob" :: ll -> option_glob := true; parse ll + | "-noglob" :: ll | "-no-glob" :: ll -> option_noglob := true; parse ll | "-I" :: r :: ll -> add_dir add_known r []; parse ll | "-I" :: [] -> usage () | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll |