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 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src/tac2stdlib.ml')

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
-- 
cgit v1.2.3