Skip to content

Commit

Permalink
[gramlib] Wrap Gramlib.
Browse files Browse the repository at this point in the history
This introduces a bit of noise in the Dune files but for now I think
it is the best way to do it.
  • Loading branch information
ejgallego committed Oct 29, 2018
1 parent 46ac539 commit cd8b897
Show file tree
Hide file tree
Showing 10 changed files with 11 additions and 4 deletions.
3 changes: 1 addition & 2 deletions gramlib/dune
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
(library
(name gramlib)
(public_name coq.gramlib)
(wrapped false))
(public_name coq.gramlib))
3 changes: 2 additions & 1 deletion parsing/dune
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,8 @@
(name parsing)
(public_name coq.parsing)
(wrapped false)
(libraries proofs))
(flags :standard -open Gramlib)
(libraries coq.gramlib proofs))

(rule
(targets g_prim.ml)
Expand Down
1 change: 1 addition & 0 deletions plugins/funind/plugin_base.dune
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,5 @@
(name recdef_plugin)
(public_name coq.plugins.recdef)
(synopsis "Coq's functional induction plugin")
(flags :standard -open Gramlib)
(libraries coq.plugins.extraction))
1 change: 1 addition & 0 deletions plugins/ltac/plugin_base.dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
(public_name coq.plugins.ltac)
(synopsis "Coq's LTAC tactic language")
(modules :standard \ tauto)
(flags :standard -open Gramlib)
(libraries coq.stm))

(library
Expand Down
1 change: 1 addition & 0 deletions plugins/ssr/plugin_base.dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@
(public_name coq.plugins.ssreflect)
(synopsis "Coq's ssreflect plugin")
(modules_without_implementation ssrast)
(flags :standard -open Gramlib)
(libraries coq.plugins.ssrmatching))
1 change: 1 addition & 0 deletions plugins/ssrmatching/plugin_base.dune
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,5 @@
(name ssrmatching_plugin)
(public_name coq.plugins.ssrmatching)
(synopsis "Coq ssrmatching plugin")
(flags :standard -open Gramlib)
(libraries coq.plugins.ltac))
2 changes: 1 addition & 1 deletion pretyping/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@
(synopsis "Coq's Type Inference Component (Pretyper)")
(public_name coq.pretyping)
(wrapped false)
(libraries coq.gramlib engine))
(libraries engine))
1 change: 1 addition & 0 deletions printing/dune
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,6 @@
(name printing)
(synopsis "Coq's Term Pretty Printing Library")
(public_name coq.printing)
(flags :standard -open Gramlib)
(wrapped false)
(libraries parsing proofs))
1 change: 1 addition & 0 deletions toplevel/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
(public_name coq.toplevel)
(synopsis "Coq's Interactive Shell [terminal-based]")
(wrapped false)
(flags :standard -open Gramlib)
(libraries num coq.stm))
; Coqlevel provides the `Num` library to plugins, we could also use
; -linkall in the plugins file, to be discussed.
Expand Down
1 change: 1 addition & 0 deletions vernac/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
(synopsis "Coq's Vernacular Language")
(public_name coq.vernac)
(wrapped false)
(flags :standard -open Gramlib)
(libraries tactics parsing))

(rule
Expand Down

0 comments on commit cd8b897

Please sign in to comment.