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 a957f7354f..f89fb9f52d 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -127,7 +127,7 @@ let classify_vernac e =
| VernacAssumption (_,_,l) ->
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in
VtSideff (ids, VtLater)
- | VernacPrimitive (id,_,_) ->
+ | VernacPrimitive ((id,_),_,_) ->
VtSideff ([id.CAst.v], VtLater)
| VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
| VernacInductive (_,l) ->