diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 4 | ||||
| -rw-r--r-- | tools/coqc.ml | 3 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 1 | ||||
| -rw-r--r-- | tools/gallina-db.el | 2 |
4 files changed, 4 insertions, 6 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ac69a69a4a..b7dd5f2a14 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -390,7 +390,7 @@ let clean sds sps = let () = if !some_vfile then let () = print "cleanall:: clean\n" in - print "\trm -f $(patsubst %.v,.%.aux,$(VFILES))\n\n" in + print "\trm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)\n\n" in print "archclean::\n"; print "\trm -f *.cmx *.o\n"; List.iter @@ -887,7 +887,7 @@ let merlin targets (ml_inc,_,_) = print ".merlin:\n"; print "\t@echo 'FLG -rectypes' > .merlin\n" ; List.iter (fun c -> - printf "\t@echo \"B $(COQLIB) %s\" >> .merlin\n" c) + printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c) lib_dirs ; List.iter (fun (_,c) -> printf "\t@echo \"B %s\" >> .merlin\n" c; diff --git a/tools/coqc.ml b/tools/coqc.ml index ecbbfefac6..b12d48710f 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -94,7 +94,6 @@ let parse_args () = |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" |"-impredicative-set"|"-vm"|"-native-compiler" - |"-verbose-compat-notations"|"-no-compat-notations" |"-indices-matter"|"-quick"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" as o) :: rem -> @@ -107,7 +106,7 @@ let parse_args () = |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" - |"-o" + |"-o"|"-profile-ltac-cutoff" as o) :: rem -> begin match rem with diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index cc63c13d7b..0064aebdae 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -526,7 +526,6 @@ let rec add_directory recur add_file phys_dir log_dir = | FileRegular f -> add_file phys_dir log_dir f in - check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir; if exists_dir phys_dir then process_directory f phys_dir else diff --git a/tools/gallina-db.el b/tools/gallina-db.el index baabebb13a..9664f69f8b 100644 --- a/tools/gallina-db.el +++ b/tools/gallina-db.el @@ -163,7 +163,7 @@ for DB structure." (defun coq-sort-menu-entries (menu) (sort menu - '(lambda (x y) (string< + (lambda (x y) (string< (downcase (elt x 0)) (downcase (elt y 0)))))) |