diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-18 15:52:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-18 15:52:11 +0200 |
| commit | 60354f102ab60c1df24ebb269b51e6664eb70aa3 (patch) | |
| tree | 44bf3392cc55857d424e0a9691d3139de40827d3 /stm/proofBlockDelimiter.ml | |
| parent | dff1450d43909e8aeaf8ce2db8bc19be42ee1ab1 (diff) | |
[stm] Fix record field name clash.
PR#173 introduced a record field name clash in `stm.mli`, with duplicate
fields `start/stop` for the types `focus` and `static_block_declaration`.
We fix by renaming the younger ones (as to minimize code
incompatibilities), but other options are possible/could be preferred,
however they would be quite more invasive so I think they should be
postponed for the day the Stm API is cleaned up.
Diffstat (limited to 'stm/proofBlockDelimiter.ml')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index ce12185cb..8162fc3bb 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -83,7 +83,7 @@ let static_bullet ({ entry_point; prev_node } as view) = if node.indentation > base then `Cont node else match node.ast with | Vernacexpr.VernacBullet b' when b = b' -> - `Found { stop = entry_point.id; start = prev.id; + `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = of_bullet_val b } | _ -> `Stop) entry_point | _ -> assert false @@ -108,7 +108,7 @@ let static_curly_brace ({ entry_point; prev_node } as view) = crawl view (fun (nesting,prev) node -> match node.ast with | Vernacexpr.VernacSubproof _ when nesting = 0 -> - `Found { stop = entry_point.id; start = prev.id; + `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = unit_val } | Vernacexpr.VernacSubproof _ -> `Cont (nesting - 1,node) @@ -135,7 +135,7 @@ let static_par { entry_point; prev_node } = match prev_node entry_point with | None -> None | Some { id = pid } -> - Some { stop = entry_point.id; start = pid; + Some { block_stop = entry_point.id; block_start = pid; dynamic_switch = pid; carry_on_data = unit_val } let dynamic_par { dynamic_switch = id } = @@ -162,7 +162,7 @@ let static_indent ({ entry_point; prev_node } as view) = crawl view ~init:(Some last_tac) (fun prev node -> if node.indentation >= last_tac.indentation then `Cont node else - `Found { stop = entry_point.id; start = node.id; + `Found { block_stop = entry_point.id; block_start = node.id; dynamic_switch = node.id; carry_on_data = of_vernac_expr_val entry_point.ast } ) last_tac |