aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-05-23 17:07:07 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-05-27 17:28:44 +0200
commit67d6eea4c34efc76bfe33ccd2476245958433ecc (patch)
tree06595c2e592d11d51cbf5fc7ac9e7afac9744a3a /plugins/ltac
parent2eb27e56ea4764fa2f2acec6f951eef2642ff1be (diff)
Exporting a few primitive tacticals as named Ltac definitions.
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.ml432
1 files changed, 32 insertions, 0 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 6890b3198..0a13a20a9 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -326,3 +326,35 @@ let initial_atomic () =
]
let () = Mltop.declare_cache_obj initial_atomic "coretactics"
+
+(* First-class Ltac access to primitive blocks *)
+
+let initial_name s = { mltac_plugin = "coretactics"; mltac_tactic = s; }
+let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; }
+
+let register_list_tactical name f =
+ let tac args ist = match args with
+ | [v] ->
+ begin match Tacinterp.Value.to_list v with
+ | None -> Tacticals.New.tclZEROMSG (Pp.str "Expected a list")
+ | Some tacs ->
+ let tacs = List.map (fun tac -> Tacinterp.tactic_of_value ist tac) tacs in
+ f tacs
+ end
+ | _ -> assert false
+ in
+ Tacenv.register_ml_tactic (initial_name name) [|tac|]
+
+let () = register_list_tactical "first" Tacticals.New.tclFIRST
+let () = register_list_tactical "solve" Tacticals.New.tclSOLVE
+
+let initial_tacticals () =
+ let idn n = Id.of_string (Printf.sprintf "_%i" n) in
+ let varn n = Reference (ArgVar (None, idn n)) in
+ let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
+ List.iter iter [
+ "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0])));
+ "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0])));
+ ]
+
+let () = Mltop.declare_cache_obj initial_tacticals "coretactics"