diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-01 23:23:14 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-01 23:23:14 +0100 |
| commit | 97c1dfa2f76a61992e600be4f07babb5be9c521e (patch) | |
| tree | dd284ed64bd38afe80966b3bab130a807e668cf5 /stm/vernac_classifier.ml | |
| parent | beab8bdff2daec9012c12648cad3f9b458a78124 (diff) | |
Remove useless recursive flags.
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
1 files changed, 1 insertions, 1 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"]),_) |