Skip to content

Commit

Permalink
nit on fmt
Browse files Browse the repository at this point in the history
  • Loading branch information
ejgallego committed Feb 15, 2023
1 parent f5bb617 commit 40cf809
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 4 deletions.
7 changes: 6 additions & 1 deletion coq/dune
Original file line number Diff line number Diff line change
Expand Up @@ -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))
5 changes: 3 additions & 2 deletions coq/parsing.ml
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
let bp_ = ref 0

let undamage_jf loc =
Loc.
{ loc with
Expand All @@ -22,6 +23,7 @@ end

module Parsable = struct
include Pcoq.Parsable

let loc = PCoqHack.loc
end

Expand All @@ -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
Expand Down
1 change: 0 additions & 1 deletion coq/parsing.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 40cf809

Please sign in to comment.