aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml18
-rw-r--r--tools/coqc.ml2
-rw-r--r--tools/coqdep.ml4
-rw-r--r--tools/coqdep_common.ml1
-rw-r--r--tools/coqdoc/cpretty.mll30
-rw-r--r--tools/coqmktop.ml4
-rw-r--r--tools/fake_ide.ml2
7 files changed, 22 insertions, 39 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 65b2441f7d..ac69a69a4a 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -141,8 +141,8 @@ let standard opt =
print "\"\n\n"
let classify_files_by_root var files (inc_ml,inc_i,inc_r) =
- if List.exists (fun (pdir,_,_) -> pdir = ".") inc_r
- || List.exists (fun (pdir,_,_) -> pdir = ".") inc_i
+ if List.exists (fun (pdir,_,_) -> pdir = ".") inc_r ||
+ List.exists (fun (pdir,_,_) -> pdir = ".") inc_i
then ()
else
let absdir_of_files =List.rev_map
@@ -207,7 +207,7 @@ let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) =
(fun x -> x^string_of_int i)
in
let pdir' = physical_dir_of_logical_dir ldir in
- (pdir,pdir',vars_r)::out) 1 [] l
+ (pdir,pdir',vars_r)::out) 0 [] l
in (Some varq, other)
let install_include_by_root perms =
@@ -465,10 +465,10 @@ let implicit () =
in
let v_rules () =
print "$(VOFILES): %.vo: %.v\n";
- print "\t$(SHOW)COQC $*\n";
- print "\t$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
- print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
- print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n";
+ print "\t$(SHOW)COQC $<\n";
+ print "\t$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n";
+ print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n";
+ print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<\n\n";
print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n";
print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n";
print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
@@ -477,7 +477,7 @@ let implicit () =
print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n";
print "\t$(SHOW)'COQDEP $<'\n";
print "\t$(HIDE)$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
- print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n"
+ print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v\n\n"
in
if !some_mlifile then mli_rules ();
if !some_ml4file then ml4_rules ();
@@ -582,7 +582,7 @@ let parameters () =
print "define donewline\n\n\nendef\n";
print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n";
print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n";
- print "TIMED?=\nTIMECMD?=\nSTDTIME=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
+ print "TIMED?=\nTIMECMD?=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
print "vo_to_obj = $(addsuffix .o,\\\n";
print " $(filter-out Warning: Error:,\\\n";
diff --git a/tools/coqc.ml b/tools/coqc.ml
index ecbbfefac6..b59bbdb1e0 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -107,7 +107,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.ml b/tools/coqdep.ml
index 9886b263cb..a7c32e1d65 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -495,7 +495,7 @@ let coqdep () =
add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
end else begin
- Envars.set_coqlib ~fail:Errors.error;
+ Envars.set_coqlib ~fail:CErrors.error;
let coqlib = Envars.coqlib () in
add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
@@ -525,6 +525,6 @@ let coqdep () =
let _ =
try
coqdep ()
- with Errors.UserError(s,p) ->
+ with CErrors.UserError(s,p) ->
let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in
Feedback.msg_error pp
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/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 005ffdae72..919f37b91b 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -675,7 +675,7 @@ and doc_bol = parse
in
match check_start_list line with
| Neither -> backtrack_past_newline lexbuf; doc None lexbuf
- | List n -> Output.paragraph ();
+ | List n -> if lines > 0 then Output.paragraph ();
Output.item 1; doc (Some [n]) lexbuf
| Rule -> Output.rule (); doc None lexbuf
}
@@ -736,24 +736,7 @@ and doc_list_bol indents = parse
in
let (n_spaces,_) = count_spaces buf in
match find_level indents n_spaces with
- | InLevel _ ->
- Output.paragraph ();
- backtrack_past_newline lexbuf;
- doc_list_bol indents lexbuf
- | StartLevel n ->
- if n = 1 then
- begin
- Output.stop_item ();
- backtrack_past_newline lexbuf;
- doc_bol lexbuf
- end
- else
- begin
- Output.paragraph ();
- backtrack_past_newline lexbuf;
- doc_list_bol indents lexbuf
- end
- | Before ->
+ | StartLevel 1 | Before ->
(* Here we were at the beginning of a line, and it was blank.
The next line started before any list items. So: insert
a paragraph for the empty line, rewind to whatever's just
@@ -763,6 +746,10 @@ and doc_list_bol indents = parse
Output.paragraph ();
backtrack_past_newline lexbuf;
doc_bol lexbuf
+ | StartLevel _ | InLevel _ ->
+ Output.paragraph ();
+ backtrack_past_newline lexbuf;
+ doc_list_bol indents lexbuf
}
| space* _
@@ -771,10 +758,7 @@ and doc_list_bol indents = parse
| Before -> Output.stop_item (); backtrack lexbuf;
doc_bol lexbuf
| StartLevel n ->
- (if n = 1 then
- Output.stop_item ()
- else
- Output.reach_item_level (n-1));
+ Output.reach_item_level (n-1);
backtrack lexbuf;
doc (Some (take (n-1) indents)) lexbuf
| InLevel (n,_) ->
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 6f3d8e2b8f..eaf938e8ce 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -235,7 +235,7 @@ let declare_loading_string () =
\n Mltop.set_top\
\n {Mltop.load_obj=\
\n (fun f -> if not (Topdirs.load_file ppf f)\
-\n then Errors.error (\"Could not load plugin \"^f));\
+\n then CErrors.error (\"Could not load plugin \"^f));\
\n Mltop.use_file=Topdirs.dir_use ppf;\
\n Mltop.add_dir=Topdirs.dir_directory;\
\n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\
@@ -265,7 +265,7 @@ let create_tmp_main_file modules =
let main () =
let (options, userfiles) = parse_args () in
(* Directories: *)
- let () = Envars.set_coqlib ~fail:Errors.error in
+ let () = Envars.set_coqlib ~fail:CErrors.error in
let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in
(* Which ocaml compiler to invoke *)
let prog = if !opt then "opt" else "ocamlc" in
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 221fb36d8d..8fcca535d1 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -38,7 +38,7 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
let rec loop () =
let xml = Xml_parser.parse coqtop.xml_parser in
match Xmlprotocol.is_message xml with
- | Some (level, content) ->
+ | Some (level, _loc, content) ->
logger level content;
loop ()
| None ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 13:42:40 +0000