diff options
| author | Pierre-Marie Pédrot | 2017-09-05 17:19:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 17:31:58 +0200 |
| commit | 53c63e43a3daf99cf8bd44498b1c53798a8ba876 (patch) | |
| tree | 1f54d9b7e4049ac8bd7dc7ac2629aac9a25e81cf /src | |
| parent | fb8142bb2fd84b10f4536fa63c972286365413f8 (diff) | |
Binding the firstorder tactic.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2stdlib.ml | 9 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 11 | ||||
| -rw-r--r-- | src/tac2tactics.mli | 2 |
3 files changed, 22 insertions, 0 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 |