diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-05 10:47:44 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-05 10:47:44 +0100 |
| commit | 55b2a4e0c24d691b71256c91ed54e245efce340b (patch) | |
| tree | 25c65622b9e9e83271d321f399981438b83ff053 /stm/stm.ml | |
| parent | f5cf5e062bdc6264dc3c398ad76559ec188cde47 (diff) | |
| parent | 5b8b60508d74bfe5e436ce182889ad8ee6ca3983 (diff) | |
Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 07d8b39bd..1b649194d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -566,8 +566,8 @@ end = struct (* {{{ *) let reachable id = reachable !vcs id let mk_branch_name { expr = x } = Branch.make (match Vernacprop.under_control x with - | VernacDefinition (_,((_,i),_),_) -> Id.to_string i - | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Id.to_string i + | VernacDefinition (_,((_, Name 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 |