aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--stm/texmacspp.ml3
-rw-r--r--tools/coqdep_common.ml5
2 files changed, 0 insertions, 8 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 1996d35259..b18e35a472 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -20,9 +20,6 @@ let unlock loc =
let start, stop = Loc.unloc loc in
(string_of_int start, string_of_int stop)
-let xmlNoop = (* almost noop *)
- PCData ""
-
let xmlWithLoc loc ename attr xml =
let start, stop = unlock loc in
Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index b66529bb38..65fbd628a5 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -165,11 +165,6 @@ let warning_module_notfound f s =
eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!"
f (String.concat "." s)
-let warning_notfound f s =
- eprintf "*** Warning: in file %s, the file " f;
- eprintf "%s.v is required and has not been found!\n" s;
- flush stderr
-
let warning_declare f s =
eprintf "*** Warning: in file %s, declared ML module " f;
eprintf "%s has not been found!\n" s;