diff options
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 1234e15afc..50e68852f8 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -115,7 +115,7 @@ let rec classify_vernac e = VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater | VernacDefinition (_,((_,i),_),ProveBody _) -> VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater - | VernacStartTheoremProof (_,l,_) -> + | VernacStartTheoremProof (_,l) -> let ids = CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater |