[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.

8 files changed, 22 insertions, 12 deletions

diff --git a/src/dune b/src/dune
new file mode 100644
index 0000000000..b0140aa809
--- /dev/null
+++ b/src/dune
@@ -0,0 +1,10 @@
+(library
+ (name ltac2)
+ (public_name coq.plugins.ltac2)
+ (modules_without_implementation tac2expr tac2qexpr tac2types)
+ (libraries coq.plugins.firstorder))
+
+(rule
+ (targets g_ltac2.ml)
+ (deps (:pp-file g_ltac2.ml4) )
+ (action (run coqp5 -loc loc -impl %{pp-file} -o %{targets})))
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 6ff353ce30..8ee239f803 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -20,8 +20,8 @@ open Proofview.Notations
 module Value = Tac2ffi
 open Value
 
-let std_core n = KerName.make2 Tac2env.std_prefix (Label.of_id (Id.of_string_soft n))
-let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
+let std_core n = KerName.make Tac2env.std_prefix (Label.of_id (Id.of_string_soft n))
+let coq_core n = KerName.make Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
 
 module Core =
 struct
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index ec10dea777..bba4680a72 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -805,7 +805,7 @@ let pr_frame = function
 
 let () = register_handler begin function
 | Tac2interp.LtacError (kn, args) ->
-  let t_exn = KerName.make2 Tac2env.coq_prefix (Label.make "exn") in
+  let t_exn = KerName.make Tac2env.coq_prefix (Label.make "exn") in
   let v = Tac2ffi.of_open (kn, args) in
   let t = GTypRef (Other t_exn, []) in
   let c = Tac2print.pr_valexpr (Global.env ()) Evd.empty v t in
@@ -897,7 +897,7 @@ let register_prim_alg name params def =
   let def = { typdef_local = false; typdef_expr = def } in
   ignore (Lib.add_leaf id (inTypDef def))
 
-let coq_def n = KerName.make2 Tac2env.coq_prefix (Label.make n)
+let coq_def n = KerName.make Tac2env.coq_prefix (Label.make n)
 
 let def_unit = {
   typdef_local = false;
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index a719970a57..df1857c3e7 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -229,7 +229,7 @@ let internal_err =
   let coq_prefix =
     MPfile (DirPath.make (List.map Id.of_string ["Init"; "Ltac2"]))
   in
-  KerName.make2 coq_prefix (Label.of_id (Id.of_string "Internal"))
+  KerName.make coq_prefix (Label.of_id (Id.of_string "Internal"))
 
 (** FIXME: handle backtrace in Ltac2 exceptions *)
 let of_exn c = match fst c with
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"
diff --git a/src/tac2match.ml b/src/tac2match.ml
index a3140eabea..c9e549d47e 100644
--- a/src/tac2match.ml
+++ b/src/tac2match.ml
@@ -181,7 +181,7 @@ module PatternMatching (E:StaticEnvironment) = struct
     pattern_match_term pat (NamedDecl.get_type decl) >>= fun ctx ->
     return (id, ctx)
 
-  let hyp_match_body_and_type bodypat typepat hyps =
+  let _hyp_match_body_and_type bodypat typepat hyps =
     pick hyps >>= function
       | LocalDef (id,body,hyp) ->
           pattern_match_term bodypat body >>= fun ctx_body ->
diff --git a/src/tac2print.ml b/src/tac2print.ml
index 0fea07ee3a..0b20cf9f58 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -22,7 +22,7 @@ let change_kn_label kn id =
 let paren p = hov 2 (str "(" ++ p ++ str ")")
 
 let t_list =
-  KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string "list"))
+  KerName.make Tac2env.coq_prefix (Label.of_id (Id.of_string "list"))
 
 
 (** Type printing *)
@@ -35,7 +35,7 @@ type typ_level =
 | T0
 
 let t_unit =
-  KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string "unit"))
+  KerName.make Tac2env.coq_prefix (Label.of_id (Id.of_string "unit"))
 
 let pr_typref kn =
   Libnames.pr_qualid (Tac2env.shortest_qualid_of_type kn)
@@ -435,7 +435,7 @@ and pr_val_list env sigma args tpe =
   str "[" ++ prlist_with_sep pr_semicolon pr args ++ str "]"
 
 let register_init n f =
-  let kn = KerName.make2 Tac2env.coq_prefix (Label.make n) in
+  let kn = KerName.make Tac2env.coq_prefix (Label.make n) in
   register_val_printer kn { val_printer = fun env sigma v _ -> f env sigma v }
 
 let () = register_init "int" begin fun _ _ n ->
@@ -476,7 +476,7 @@ let () = register_init "err" begin fun _ _ e ->
 end
 
 let () =
-  let kn = KerName.make2 Tac2env.coq_prefix (Label.make "array") in
+  let kn = KerName.make Tac2env.coq_prefix (Label.make "array") in
   let val_printer env sigma v arg = match arg with
   | [arg] ->
     let (_, v) = to_block v in
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 1d742afd83..3bddfe7594 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -32,7 +32,7 @@ let control_prefix = prefix_gen "Control"
 let pattern_prefix = prefix_gen "Pattern"
 let array_prefix = prefix_gen "Array"
 
-let kername prefix n = KerName.make2 prefix (Label.of_id (Id.of_string_soft n))
+let kername prefix n = KerName.make prefix (Label.of_id (Id.of_string_soft n))
 let std_core n = kername Tac2env.std_prefix n
 let coq_core n = kername Tac2env.coq_prefix n
 let control_core n = kername control_prefix n