Skip to content

Commit

Permalink
[v8.17] Coq 8.17 is now sane for multiple documents.
Browse files Browse the repository at this point in the history
  • Loading branch information
ejgallego committed Apr 3, 2023
1 parent 029154b commit 36467bd
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 3 deletions.
4 changes: 2 additions & 2 deletions controller/doc_manager.ml
Original file line number Diff line number Diff line change
Expand Up @@ -227,8 +227,8 @@ let create ~ofmt ~root_state ~workspace ~uri ~raw ~version =
send_error_permanent_fail ~ofmt ~uri ~version (Pp.str message)
| Interrupted -> ()

(* Set this to false for < 8.18, we could parse the version but not worth it. *)
let sane_coq_base_version = false
(* Set this to false for < 8.17, we could parse the version but not worth it. *)
let sane_coq_base_version = true

let sane_coq_branch =
CString.string_contains ~where:Coq_config.version ~what:"+lsp"
Expand Down
6 changes: 5 additions & 1 deletion coq/parsing.ml
Original file line number Diff line number Diff line change
@@ -1,4 +1,8 @@
module Parsable = Pcoq.Parsable
module Parsable = struct
include Pcoq.Parsable

let make = make ?fix_loc:None
end

let parse ~st ps =
let mode = State.mode ~st in
Expand Down

0 comments on commit 36467bd

Please sign in to comment.