adapt to API.mli removal

4 files changed, 4 insertions, 14 deletions

diff --git a/_CoqProject b/_CoqProject
index eec66dc75e..5af42197ea 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,5 @@
 -R theories/ Ltac2
 -I src/
--bypass-API
 
 src/tac2dyn.ml
 src/tac2dyn.mli
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index c738cb65bd..31eb6d9db5 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -91,8 +91,7 @@ let tac2def_mut = Gram.entry_create "tactic:tac2def_mut"
 let tac2def_run = Gram.entry_create "tactic:tac2def_run"
 let tac2mode = Gram.entry_create "vernac:ltac2_command"
 
-(** FUCK YOU API *)
-let ltac1_expr = (Obj.magic Pltac.tactic_expr : Tacexpr.raw_tactic_expr Gram.entry)
+let ltac1_expr = Pltac.tactic_expr
 
 let inj_wit wit loc x = Loc.tag ~loc @@ CTacExt (wit, x)
 let inj_open_constr loc c = inj_wit Tac2quote.wit_open_constr loc c
diff --git a/src/tac2core.ml b/src/tac2core.ml
index d21c1998da..295b1b24ec 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -945,8 +945,7 @@ let () =
     let ist = { env_ist = Id.Map.empty } in
     let lfun = Tac2interp.set_env ist Id.Map.empty in
     let ist = Ltac_plugin.Tacinterp.default_ist () in
-    (** FUCK YOU API *)
-    let ist = { ist with API.Geninterp.lfun = (Obj.magic lfun) } in
+    let ist = { ist with Geninterp.lfun = lfun } in
     let tac = (Obj.magic Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in
     let wrap (e, info) = set_bt info >>= fun info -> Proofview.tclZERO ~info e in
     Proofview.tclOR tac wrap >>= fun () ->
@@ -995,8 +994,7 @@ let () =
 (** Ltac2 in Ltac1 *)
 
 let () =
-  (** FUCK YOU API *)
-  let e = (Obj.magic Tac2entries.Pltac.tac2expr : _ API.Pcoq.Gram.entry) in
+  let e = Tac2entries.Pltac.tac2expr in
   let inject (loc, v) = Tacexpr.TacGeneric (in_gen (rawwit wit_ltac2) v) in
   Ltac_plugin.Tacentries.create_ltac_quotation "ltac2" inject (e, None)
 
@@ -1004,8 +1002,6 @@ let () =
   let open Ltac_plugin in
   let open Tacinterp in
   let idtac = Value.of_closure (default_ist ()) (Tacexpr.TacId []) in
-  (** FUCK YOU API *)
-  let idtac = (Obj.magic idtac : Geninterp.Val.t) in
   let interp ist tac =
 (*     let ist = Tac2interp.get_env ist.Geninterp.lfun in *)
     let ist = { env_ist = Id.Map.empty } in
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index cd5709b130..e7d5578b6e 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -448,10 +448,6 @@ let contradiction c =
 
 let firstorder tac refs ids =
   let open Ground_plugin in
-  (** FUCK YOU API *)
   let ids = List.map Id.to_string ids in
   let tac = Option.map (fun tac -> thaw Tac2ffi.unit tac) tac in
-  let tac : unit API.Proofview.tactic option = Obj.magic (tac : unit Proofview.tactic option) in
-  let refs : API.Globnames.global_reference list = Obj.magic (refs : Globnames.global_reference list) in
-  let ids : API.Hints.hint_db_name list = Obj.magic (ids : Hints.hint_db_name list) in
-  (Obj.magic (G_ground.gen_ground_tac true tac refs ids : unit API.Proofview.tactic) : unit Proofview.tactic)
+  G_ground.gen_ground_tac true tac refs ids