Skip to content

Commit

Permalink
refactor(coq): minor tweaks
Browse files Browse the repository at this point in the history
Signed-off-by: Ali Caglayan <[email protected]>

ps-id: 82c51d60-647a-44bd-aec8-1ff7495d4290
  • Loading branch information
Alizter authored and ejgallego committed Oct 7, 2022
1 parent 01fe246 commit b423d7c
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions src/dune_rules/coq_rules.ml
Original file line number Diff line number Diff line change
Expand Up @@ -584,8 +584,9 @@ let setup_coqdoc_rules ~sctx ~dir ~cctx (s : Theory.t) coq_modules =
|> Path.build |> Action_builder.path
|> Rules.Produce.Alias.add_deps (Coqdoc_mode.alias mode ~dir) ~loc
in
let* () = rule Html in
rule Latex
let+ () = rule Html
and+ () = rule Latex in
()

let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
let theory =
Expand All @@ -597,8 +598,8 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
let* cctx, coq_modules =
setup_cctx_and_modules ~sctx ~dir ~dir_contents s theory
in
let* () = setup_vo_rules ~sctx ~dir ~cctx s theory coq_modules in
let+ () = setup_coqdoc_rules ~sctx ~dir ~cctx s coq_modules in
let+ () = setup_vo_rules ~sctx ~dir ~cctx s theory coq_modules
and+ () = setup_coqdoc_rules ~sctx ~dir ~cctx s coq_modules in
()

let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Theory.t) coq_module =
Expand Down Expand Up @@ -716,7 +717,7 @@ let setup_coqpp_rules ~sctx ~dir (s : Coqpp.t) =

let setup_extraction_cctx_and_modules ~sctx ~dir ~dir_contents
(s : Extraction.t) =
let* cctx =
let+ cctx =
let wrapper_name = "DuneExtraction" in
let* theories_deps =
let* scope = Scope.DB.find_by_dir dir in
Expand All @@ -728,8 +729,7 @@ let setup_extraction_cctx_and_modules ~sctx ~dir ~dir_contents
let theories_deps = Resolve.Memo.lift theories_deps in
Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps
~theory_dirs s.buildable
in
let+ coq = Dir_contents.coq dir_contents in
and+ coq = Dir_contents.coq dir_contents in
(cctx, Coq_sources.extract coq s)

let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) =
Expand Down

0 comments on commit b423d7c

Please sign in to comment.