diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-23 17:14:24 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-23 17:14:24 +0200 |
| commit | f258dd1954f4ab738a987798630cfaaddfb9de37 (patch) | |
| tree | 8f5d1f02f307156075c2f952aab1de3daf489cd7 /stm | |
| parent | 7cc335bd4cc568bdf892da60ebd16e6acfe019cd (diff) | |
| parent | 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 (diff) | |
Merge PR#821: [vernac] Remove stale bool parameter from `VernacStartTheoremProof`
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index b9247fff0..01edc9d2d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -476,7 +476,7 @@ end = struct (* {{{ *) let mk_branch_name { expr = x } = Branch.make (let rec aux x = match x with | VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i - | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> Names.string_of_id i + | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.string_of_id i | VernacTime (_, e) | VernacTimeout (_, e) -> aux e | _ -> "branch" in aux x) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 1234e15af..50e68852f 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 |