diff options
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2a6a47b02..cbbb54e45 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -93,8 +93,7 @@ let classify_vernac e = let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> - let ids = - CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in + let ids = List.map (fun (((_, i), _), _) -> i) l in let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof (default_proof_mode (),guarantee,ids), VtLater | VernacFixpoint (discharge,l) -> |