diff options
| author | Vincent Laporte | 2018-01-25 16:52:00 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-02-01 16:20:16 +0000 |
| commit | 5b8b60508d74bfe5e436ce182889ad8ee6ca3983 (patch) | |
| tree | 3a9bdfb906444e1f041af3e09df0cc49f911839b /stm | |
| parent | e42f575b22ff2d2a69951227e8c2dd67fd0ab3ee (diff) | |
[vernac] Mutual theorems (VernacStartTheoremProof) always have names
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index ba6c900114..ef599fd486 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -548,7 +548,7 @@ end = struct (* {{{ *) let mk_branch_name { expr = x } = Branch.make (match Vernacprop.under_control x with | VernacDefinition (_,((_, Name i),_),_) -> Id.to_string i - | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Id.to_string i + | VernacStartTheoremProof (_,[((_,i),_),_]) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2a6a47b020..cbbb54e45b 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) -> |