diff options
| author | Emilio Jesus Gallego Arias | 2018-10-17 02:02:20 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-17 02:05:31 +0200 |
| commit | 8b9b1be48a9c83f70cbfb70f52eabc616065fa1e (patch) | |
| tree | edbe6a709cea1379c6a7bad7ef5605e5cfc055ae /src/tac2intern.ml | |
| parent | 120a8020f6b98ea00988cc37641944811832d139 (diff) | |
[build] Add dune file + fix warnings.
This allows to drop the ltac2 folder inside the Coq dir and have it
compose with the Coq build.
I've fixed build warnings by the way.
Diffstat (limited to 'src/tac2intern.ml')
| -rw-r--r-- | src/tac2intern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2intern.ml b/src/tac2intern.ml index ff8fb4c0f4..fe615853ce 100644 --- a/src/tac2intern.ml +++ b/src/tac2intern.ml @@ -19,7 +19,7 @@ open Tac2expr (** Hardwired types and constants *) -let coq_type n = KerName.make2 Tac2env.coq_prefix (Label.make n) +let coq_type n = KerName.make Tac2env.coq_prefix (Label.make n) let t_int = coq_type "int" let t_string = coq_type "string" |