@@ -117,19 +117,18 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
117
117
match classif with
118
118
| VtStartProof (_ , names ) ->
119
119
let vernac_gen_expr = ast.v.expr in
120
- let type_ =
121
- begin match vernac_gen_expr with
120
+ let type_ = match vernac_gen_expr with
122
121
| VernacSynterp _ -> None
123
122
| VernacSynPure pure ->
124
123
match pure with
125
124
| Vernacexpr. VernacStartTheoremProof (kind , _ ) -> Some (TheoremKind kind)
126
125
| Vernacexpr. VernacDefinition ((_ , def ), _ , _ ) -> Some (DefinitionType def)
127
126
| _ -> None
128
- end in
129
- let name = begin match names with
127
+ in
128
+ let name = match names with
130
129
| [] -> " default"
131
130
| n :: _ -> Names.Id. to_string n
132
- end in
131
+ in
133
132
let statement = " " in
134
133
begin match type_ with
135
134
| None -> outline
@@ -140,19 +139,18 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
140
139
end
141
140
| VtSideff (names , _ ) ->
142
141
let vernac_gen_expr = ast.v.expr in
143
- let type_ =
144
- begin match vernac_gen_expr with
142
+ let type_ = match vernac_gen_expr with
145
143
| VernacSynterp _ -> None
146
144
| VernacSynPure pure ->
147
145
match pure with
148
146
| Vernacexpr. VernacStartTheoremProof (kind , _ ) -> Some (TheoremKind kind)
149
147
| Vernacexpr. VernacDefinition ((_ , def ), _ , _ ) -> Some (DefinitionType def)
150
148
| _ -> None
151
- end in
152
- let name = begin match names with
149
+ in
150
+ let name = match names with
153
151
| [] -> " default"
154
152
| n :: _ -> Names.Id. to_string n
155
- end in
153
+ in
156
154
let statement = " " in
157
155
begin match type_ with
158
156
| None -> outline
0 commit comments