aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vernac_classifier.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/vernac_classifier.ml')
-rw-r--r--stm/vernac_classifier.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index d25861d5a..1234e15af 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -139,7 +139,7 @@ let rec classify_vernac e =
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in
VtSideff ids, VtLater
| VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
- | VernacInductive (_,_,l) ->
+ | VernacInductive (_, _,_,l) ->
let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
| RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @