diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-06 11:36:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-06 11:36:16 +0000 |
| commit | c72588e26c59037fe9a9455f9796c0dfd5bc9ed1 (patch) | |
| tree | 022e41a03cf8d6da62b1cedd0913f8a5339605dc | |
| parent | 78a213bfd65176dae8418bffb4fd95ef22326c81 (diff) | |
Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard pour associer un nom physique à un nom logique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1066 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | scripts/coqc.ml | 3 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 6 | ||||
| -rw-r--r-- | toplevel/usage.ml | 2 |
4 files changed, 8 insertions, 9 deletions
@@ -44,7 +44,7 @@ OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS) CAMLP4EXTENDFLAGS=-I . pa_extend.cmo q_MLast.cmo CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p' -COQINCLUDES=-I states -R theories -as Coq -R contrib -as Coq +COQINCLUDES=-I states -R theories Coq -R contrib Coq # -I contrib/omega -I contrib/ring -I contrib/xml \ # -I theories/Init -I theories/Logic -I theories/Arith \ # -I theories/Bool -I theories/Zarith -I theories/Lists \ @@ -224,7 +224,7 @@ INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/Logic_TypeSyntax.vo theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) - $(COQC) -$(BEST) -bindir bin -q -R theories -as Coq -is states/barestate.coq $< + $(COQC) -$(BEST) -bindir bin -q -R theories Coq -is states/barestate.coq $< init: $(INITVO) @@ -235,7 +235,7 @@ tactics/%.vo: tactics/%.v states/barestate.coq $(COQC) $(COQC) -$(BEST) -bindir bin -q -I tactics -is states/barestate.coq $< states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTICSVO) $(BESTCOQTOP) - $(BESTCOQTOP) -q -batch -silent -is states/barestate.coq -I tactics -R theories -as Coq -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq + $(BESTCOQTOP) -q -batch -silent -is states/barestate.coq -I tactics -R theories Coq -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq clean:: rm -f states/*~ states/*.coq diff --git a/scripts/coqc.ml b/scripts/coqc.ml index ee77b8edb..4dc09bc18 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -123,7 +123,7 @@ let parse_args () = | "-opt" :: rem -> binary := "coqtop.opt"; parse (cfiles,args) rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-image"|"-libdir"|"-I"|"-R"|"-as"|"-include"|"-outputstate" + | ("-image"|"-libdir"|"-I"|"-include"|"-outputstate" |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" |"-init-file" as o) :: rem -> @@ -132,6 +132,7 @@ let parse_args () = | s :: rem' -> parse (cfiles,s::o::args) rem' | [] -> usage () end + | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent" as o) :: rem -> diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ebd291e37..2d6a9f2af 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -88,13 +88,11 @@ let parse_args () = let rec parse = function | [] -> () - | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p; parse rem - | "-R" :: d :: rem -> set_default_rec_include d; parse rem - | "-R" :: [] -> usage () + | "-R" :: d :: p :: rem -> set_rec_include d p; parse rem + | "-R" :: ([] | _ :: _) -> usage () | "-q" :: rem -> no_load_rc (); parse rem diff --git a/toplevel/usage.ml b/toplevel/usage.ml index dcd845e33..a0eb96e59 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -15,7 +15,7 @@ let print_usage_channel co command = output_string co " -I dir add directory dir in the include path -include dir (idem) - -R dir add dir recursively + -R dir coqdir recursively map physical dir to logical coqdir -src add source directories in the include path -inputstate f read state from file f.coq |