Binding the firstorder tactic.

5 files changed, 43 insertions, 5 deletions

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
diff --git a/theories/Notations.v b/theories/Notations.v
index 743210ae8d..9b39942ca5 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -470,14 +470,14 @@ Ltac2 default_db dbs := match dbs with
   end
 end.
 
-Ltac2 default_using use := match use with
+Ltac2 default_list use := match use with
 | None => []
 | Some use => use
 end.
 
 Ltac2 trivial0 use dbs :=
   let dbs := default_db dbs in
-  let use := default_using use in
+  let use := default_list use in
   Std.trivial Std.Off use dbs.
 
 Ltac2 Notation "trivial"
@@ -488,7 +488,7 @@ Ltac2 Notation trivial := trivial.
 
 Ltac2 auto0 n use dbs :=
   let dbs := default_db dbs in
-  let use := default_using use in
+  let use := default_list use in
   Std.auto Std.Off n use dbs.
 
 Ltac2 Notation "auto" n(opt(tactic(0)))
@@ -499,7 +499,7 @@ Ltac2 Notation auto := auto.
 
 Ltac2 new_eauto0 n use dbs :=
   let dbs := default_db dbs in
-  let use := default_using use in
+  let use := default_list use in
   Std.new_auto Std.Off n use dbs.
 
 Ltac2 Notation "new" "auto" n(opt(tactic(0)))
@@ -508,7 +508,7 @@ Ltac2 Notation "new" "auto" n(opt(tactic(0)))
 
 Ltac2 eauto0 n p use dbs :=
   let dbs := default_db dbs in
-  let use := default_using use in
+  let use := default_list use in
   Std.eauto Std.Off n p use dbs.
 
 Ltac2 Notation "eauto" n(opt(tactic(0))) p(opt(tactic(0)))
@@ -529,3 +529,15 @@ Ltac2 Notation typeclasses_eauto := typeclasses_eauto.
 
 Ltac2 f_equal0 () := ltac1:(f_equal).
 Ltac2 Notation f_equal := f_equal0 ().
+
+(** Firstorder *)
+
+Ltac2 firstorder0 tac refs ids :=
+  let refs := default_list refs in
+  let ids := default_list ids in
+  Std.firstorder tac refs ids.
+
+Ltac2 Notation "firstorder"
+  tac(opt(thunk(tactic)))
+  refs(opt(seq("using", list1(reference, ","))))
+  ids(opt(seq("with", list1(ident)))) := firstorder0 tac refs ids.
diff --git a/theories/Std.v b/theories/Std.v
index a937560b10..f8b269dce6 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -246,3 +246,7 @@ Ltac2 @ external new_auto : debug -> int option -> (unit -> constr) list -> iden
 Ltac2 @ external eauto : debug -> int option -> int option -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_eauto".
 
 Ltac2 @ external typeclasses_eauto : strategy option -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto".
+
+(** firstorder *)
+
+Ltac2 @ external firstorder : (unit -> unit) option -> reference list -> ident list -> unit := "ltac2" "tac_firstorder".