Skip to content

Commit

Permalink
Annotation
Browse files Browse the repository at this point in the history
  • Loading branch information
dlesbre authored and rtetley committed Nov 30, 2023
1 parent b229cde commit 9b38d37
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion language-server/dm/document.ml
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,7 @@ let find_sentence_after parsed loc =
| Some (_, sentence) -> Some sentence
| _ -> None

let find_next_qed (parsed : document) loc =
let find_next_qed parsed loc =
let exception Found of sentence in
let f k sentence =
if loc <= k then
Expand Down

0 comments on commit 9b38d37

Please sign in to comment.