From 97c1dfa2f76a61992e600be4f07babb5be9c521e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 1 Jan 2016 23:23:14 +0100
Subject: Remove useless recursive flags.

---
 stm/vernac_classifier.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm/vernac_classifier.ml')

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"]),_)
-- 
cgit v1.2.3