diff options
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 7cecd801e4..aa16f9535d 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -188,11 +188,11 @@ let classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow | VernacProofMode pm -> VtProofMode pm, VtNow - | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> + | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater - | VernacInstance (_,((name,_),_,_),_,_) -> + | VernacInstance ((name,_),_,_,_,_) -> VtSideff (idents_of_name name.CAst.v), VtLater (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll |