aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--stm/vernac_classifier.ml2
-rw-r--r--tools/ocamllibdep.mll2
2 files changed, 2 insertions, 2 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 58e26de84..dcb670094 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -60,7 +60,7 @@ let undo_classifier = ref (fun _ -> assert false)
let set_undo_classifier f = undo_classifier := f
let rec classify_vernac e =
- let rec static_classifier e = match e with
+ let static_classifier e = match e with
(* PG compatibility *)
| VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
| VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index 1bcbe7c0e..670ff487c 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -164,7 +164,7 @@ let traite_fichier_modules md ext =
let addQueue q v = q := v :: !q
-let rec treat_file old_name =
+let treat_file old_name =
let name = Filename.basename old_name in
let dirname = Some (Filename.dirname old_name) in
match get_extension name [".mllib"] with