diff options
| author | Emilio Jesus Gallego Arias | 2018-10-07 07:08:42 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-29 01:25:34 +0100 |
| commit | 641042302f05f6ec42f61a4bdb73fad70bb90c41 (patch) | |
| tree | 5ff17d4a38d49f631f398e82330ab84ffdf9de2a /pretyping | |
| parent | 503fa442869978a9e19e738be990ea8c7534962e (diff) | |
[camlp5] Fix warnings, switch Coq to vendored library.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/dune | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/dune b/pretyping/dune index 6609b4e328..89977cb946 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 camlp5.gramlib engine)) + (libraries coq.gramlib engine)) |