diff --git a/coq/dune b/coq/dune index 640a23f6..ec53e106 100644 --- a/coq/dune +++ b/coq/dune @@ -3,4 +3,9 @@ (public_name coq-lsp.coq) ; Unfortunate we have to link the STM due to the LTAC plugin ; depending on it, we should fix this upstream - (libraries lang coq-core.vernac coq-core.stm coq-serapi.serlib camlp-streams)) + (libraries + lang + coq-core.vernac + coq-core.stm + coq-serapi.serlib + camlp-streams)) diff --git a/coq/parsing.ml b/coq/parsing.ml index ae26a3c4..0fc3eba8 100644 --- a/coq/parsing.ml +++ b/coq/parsing.ml @@ -1,4 +1,5 @@ let bp_ = ref 0 + let undamage_jf loc = Loc. { loc with @@ -22,6 +23,7 @@ end module Parsable = struct include Pcoq.Parsable + let loc = PCoqHack.loc end @@ -32,8 +34,7 @@ let parse ~st ps = coq_protect *) Control.check_for_interrupt (); Vernacstate.Parser.parse st Pvernac.(main_entry mode) ps - |> Option.map (fun { CAst.loc; v } -> - CAst.make ?loc:(undamage_jf_opt loc) v) + |> Option.map (fun { CAst.loc; v } -> CAst.make ?loc:(undamage_jf_opt loc) v) |> Option.map Ast.of_coq let parse ~st ps = Protect.eval ~f:(parse ~st) ps diff --git a/coq/parsing.mli b/coq/parsing.mli index 0481c6d1..20039d7b 100644 --- a/coq/parsing.mli +++ b/coq/parsing.mli @@ -7,5 +7,4 @@ end val parse : st:State.t -> Parsable.t -> (Ast.t option, Loc.t) Protect.E.t val discard_to_dot : Parsable.t -> unit - val bp_ : int ref