diff options
| -rw-r--r-- | toplevel/coqtop.ml | 5 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
2 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c174877dff..c70bab141c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -151,8 +151,9 @@ let parse_args () = | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem | "-load-ml-source" :: [] -> usage () - | "-load-vernac-source" :: f :: rem -> add_load_vernacular f; parse rem - | "-load-vernac-source" :: [] -> usage () + | ("-load-vernac-source"|"-l") :: f :: rem -> + add_load_vernacular f; parse rem + | ("-load-vernac-source"|"-l") :: [] -> usage () | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem | "-load-vernac-object" :: [] -> usage () diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 277cc7ad92..962fdcf78c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -33,6 +33,7 @@ let print_usage_channel co command = -load-ml-object f load ML object file f -load-ml-source f load ML file f -load-vernac-source f load Coq file f.v (Load f.) + -l f (idem) -load-vernac-object f load Coq object file f.vo -require f load Coq object file f.vo and import it (Require f.) -compile f compile Coq file f.v (implies -batch) |