From 53c63e43a3daf99cf8bd44498b1c53798a8ba876 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Sep 2017 17:19:41 +0200
Subject: Binding the firstorder tactic.

---
 src/tac2stdlib.ml   |  9 +++++++++
 src/tac2tactics.ml  | 11 +++++++++++
 src/tac2tactics.mli |  2 ++
 3 files changed, 22 insertions(+)

(limited to 'src')

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 1762952e55..713a5f1b1c 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -705,3 +705,12 @@ let () = define_prim3 "tac_typeclasses_eauto" begin fun bt str n dbs ->
   let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in
   Tac2tactics.typeclasses_eauto str n dbs
 end
+
+(** Firstorder *)
+
+let () = define_prim3 "tac_firstorder" begin fun bt tac refs ids ->
+  let tac = Value.to_option (fun t -> Proofview.tclIGNORE (thaw bt t)) tac in
+  let refs = Value.to_list Value.to_reference refs in
+  let ids = Value.to_list Value.to_ident ids in
+  Tac2tactics.firstorder tac refs ids
+end
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index b069e57235..dacbb898d3 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -281,3 +281,14 @@ let inversion knd arg pat ids =
     end
   in
   on_destruction_arg inversion true (Some arg)
+
+(** Firstorder *)
+
+let firstorder tac refs ids =
+  let open Ground_plugin in
+  (** FUCK YOU API *)
+  let ids = List.map Id.to_string ids 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)
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 8b466cd529..841e8fe762 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -101,3 +101,5 @@ val typeclasses_eauto : Class_tactics.search_strategy option -> int option ->
   Id.t list option -> unit Proofview.tactic
 
 val inversion : inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
+
+val firstorder : unit Proofview.tactic option -> global_reference list -> Id.t list -> unit tactic
-- 
cgit v1.2.3