aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/vernac_classifier.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 292e3966a1..42540af991 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -130,6 +130,8 @@ 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,_,_) ->
+ VtSideff [id.CAst.v], VtLater
| VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id), VtLater
| VernacInductive (_, _,_,l) ->
let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with