diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-21 15:12:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-21 15:12:21 +0200 |
| commit | 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 (patch) | |
| tree | 1a62e205de6964d9cff96ae0fe3a46319206e74a /stm/stm.ml | |
| parent | d30ed5fe0694466f70eed51bc689cd0fa8c00da5 (diff) | |
[vernac] Remove stale bool parameter from `VernacStartTheoremProof`
`VernacStartTheoremProof` contained a stale bool parameter from 15
years ago, which is unused today.
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 071d2edf9..81bac6a1f 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) |