aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-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 7a30923c8a..fcfd616f40 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -126,7 +126,7 @@ let rec classify_vernac e =
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd 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] | _ -> []) @