aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-10-08 16:09:49 +0200
committerEmilio Jesus Gallego Arias2018-10-29 01:25:34 +0100
commitcd8b8974e2d62a3c3c4d7572921b5a83cbb8642c (patch)
treed0be5cca13dc62ac91829531e4906733ac35cbb7 /pretyping
parent46ac5393bf8d3dfef069c4190e3bfe6a3b4dcd90 (diff)
[gramlib] Wrap `Gramlib`.
This introduces a bit of noise in the Dune files but for now I think it is the best way to do it.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/dune b/pretyping/dune
index 89977cb946..14bce92de1 100644
--- a/pretyping/dune
+++ b/pretyping/dune
@@ -3,4 +3,4 @@
(synopsis "Coq's Type Inference Component (Pretyper)")
(public_name coq.pretyping)
(wrapped false)
- (libraries coq.gramlib engine))
+ (libraries engine))