aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml4
-rw-r--r--tools/coqdoc/output.ml2
2 files changed, 3 insertions, 3 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index f8f046ae75..3e8cafc417 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -34,7 +34,7 @@ let rec print_prefix_list sep = function
let usage_coq_makefile () =
output_string stderr "Usage summary:\
\n\
-\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\
+\ncoq_makefile .... [file.v] ... [file.ml[ig]?] ... [file.ml{lib,pack}]\
\n ... [any] ... [-extra[-phony] result dependencies command]\
\n ... [-I dir] ... [-R physicalpath logicalpath]\
\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
@@ -45,7 +45,7 @@ let usage_coq_makefile () =
\nFull list of options:\
\n\
\n[file.v]: Coq file to be compiled\
-\n[file.ml[i4]?]: Objective Caml file to be compiled\
+\n[file.ml[ig]?]: Objective Caml file to be compiled\
\n[file.ml{lib,pack}]: ocamlbuild-style file that describes a Objective Caml\
\n library/module\
\n[any] : subdirectory that should be \"made\" and has a Makefile itself\
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 717c06a868..ae1e1c6ed3 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -30,7 +30,7 @@ let build_table l =
let is_keyword =
build_table
- [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
+ [ "About"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
"CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
"Export"; "Fact"; "Fix"; "Fixpoint"; "From"; "Function"; "Generalizable"; "Global"; "Grammar";
"Guarded"; "Goal"; "Hint"; "Debug"; "On";