summaryrefslogtreecommitdiff
path: root/scripts/coqc.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-01 17:21:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-01 17:21:14 +0200
commitda178a880e3ace820b41d38b191d3785b82991f5 (patch)
tree6356ab3164a5ad629f4161dc6c44ead74edc2937 /scripts/coqc.ml
parente4282ea99c664d8d58067bee199cbbcf881b60d5 (diff)
Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg
Diffstat (limited to 'scripts/coqc.ml')
-rw-r--r--scripts/coqc.ml18
1 files changed, 14 insertions, 4 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 784e2d51..69357b2f 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqc.ml 11749 2009-01-05 14:01:04Z notin $ *)
+(* $Id: coqc.ml 12911 2010-04-09 10:08:37Z herbelin $ *)
(* Afin de rendre Coq plus portable, ce programme Caml remplace le script
coqc.
@@ -126,8 +126,8 @@ let parse_args () =
parse (cfiles,args) rem
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
- | ("-I"|"-include"|"-outputstate"
- |"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object"
+ | ("-outputstate"|"-inputstate"|"-is"
+ |"-load-vernac-source"|"-l"|"-load-vernac-object"
|"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
|"-init-file" | "-dump-glob" | "-coqlib" as o) :: rem ->
begin
@@ -135,7 +135,17 @@ 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
+ | ("-I"|"-include" as o) :: rem ->
+ begin
+ match rem with
+ | s :: "-as" :: t :: rem' -> parse (cfiles,t::"-as"::s::o::args) rem'
+ | s :: "-as" :: [] -> usage ()
+ | s :: rem' -> parse (cfiles,s::o::args) rem'
+ | [] -> usage ()
+ end
+ | "-R" :: s :: "-as" :: t :: rem -> parse (cfiles,t::"-as"::s::"-R"::args) rem
+ | "-R" :: s :: "-as" :: [] -> usage ()
+ | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
| ("-notactics"|"-debug"|"-nolib"
|"-debugVM"|"-alltransp"|"-VMno"