diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 5 | ||||
| -rw-r--r-- | src/ltac2_plugin.mlpack | 1 | ||||
| -rw-r--r-- | src/tac2core.ml | 8 | ||||
| -rw-r--r-- | src/tac2entries.ml | 1 | ||||
| -rw-r--r-- | src/tac2entries.mli | 1 | ||||
| -rw-r--r-- | src/tac2stdlib.ml | 12 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 25 | ||||
| -rw-r--r-- | src/tac2tactics.mli | 18 |
8 files changed, 70 insertions, 1 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index bb98ea3e5d..ca3631799b 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -291,7 +291,7 @@ open Tac2entries.Pltac let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l)) GEXTEND Gram - GLOBAL: q_ident q_bindings q_intropatterns; + GLOBAL: q_ident q_bindings q_intropattern q_intropatterns; ident_or_anti: [ [ id = Prim.ident -> QExpr id | LEFTQMARK; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) @@ -375,6 +375,9 @@ GEXTEND Gram q_intropatterns: [ [ ipat = intropatterns -> Tac2quote.of_intro_patterns ~loc:!@loc ipat ] ] ; + q_intropattern: + [ [ ipat = simple_intropattern -> Tac2quote.of_intro_pattern ~loc:!@loc ipat ] ] + ; END (** Extension of constr syntax *) diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack index 8d2d7dc0f4..4c4082ad65 100644 --- a/src/ltac2_plugin.mlpack +++ b/src/ltac2_plugin.mlpack @@ -6,5 +6,6 @@ Tac2entries Tac2ffi Tac2core Tac2quote +Tac2tactics Tac2stdlib G_ltac2 diff --git a/src/tac2core.ml b/src/tac2core.ml index b45275210e..329c115be3 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -883,6 +883,14 @@ let () = add_scope "bindings" begin function | _ -> scope_fail () end +let () = add_scope "intropattern" begin function +| [] -> + let scope = Extend.Aentry Tac2entries.Pltac.q_intropattern in + let act tac = tac in + Tac2entries.ScopeRule (scope, act) +| _ -> scope_fail () +end + let () = add_scope "intropatterns" begin function | [] -> let scope = Extend.Aentry Tac2entries.Pltac.q_intropatterns in diff --git a/src/tac2entries.ml b/src/tac2entries.ml index 0f32736096..52a5899d25 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -26,6 +26,7 @@ let tac2expr = Pcoq.Gram.entry_create "tactic:tac2expr" let q_ident = Pcoq.Gram.entry_create "tactic:q_ident" let q_bindings = Pcoq.Gram.entry_create "tactic:q_bindings" +let q_intropattern = Pcoq.Gram.entry_create "tactic:q_intropattern" let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns" end diff --git a/src/tac2entries.mli b/src/tac2entries.mli index e5031fdba2..2e51a4fb2e 100644 --- a/src/tac2entries.mli +++ b/src/tac2entries.mli @@ -59,5 +59,6 @@ val tac2expr : raw_tacexpr Pcoq.Gram.entry val q_ident : raw_tacexpr Pcoq.Gram.entry val q_bindings : raw_tacexpr Pcoq.Gram.entry +val q_intropattern : raw_tacexpr Pcoq.Gram.entry val q_intropatterns : raw_tacexpr Pcoq.Gram.entry end diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml index f63252ec22..b678b65b82 100644 --- a/src/tac2stdlib.ml +++ b/src/tac2stdlib.ml @@ -12,6 +12,7 @@ open Misctypes open Genredexpr open Tac2expr open Tac2core +open Tac2tactics open Proofview.Notations module Value = Tac2ffi @@ -178,6 +179,17 @@ let () = define_prim2 "tac_intros" begin fun ev ipat -> Tactics.intros_patterns ev ipat end +let () = define_prim4 "tac_apply" begin fun adv ev cb ipat -> + let adv = Value.to_bool adv in + let ev = Value.to_bool ev in + let map_cb c = thaw c >>= fun c -> return (to_constr_with_bindings c) in + let cb = Value.to_list map_cb cb in + let map p = Value.to_option (fun p -> Loc.tag (to_intro_pattern p)) p in + let map_ipat p = to_pair Value.to_ident map p in + let ipat = Value.to_option map_ipat ipat in + Tac2tactics.apply adv ev cb ipat +end + let () = define_prim3 "tac_elim" begin fun ev c copt -> let ev = Value.to_bool ev in let c = to_constr_with_bindings c in diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml new file mode 100644 index 0000000000..2590d7daed --- /dev/null +++ b/src/tac2tactics.ml @@ -0,0 +1,25 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Tactics +open Tacmach.New +open Tacticals.New +open Proofview.Notations + +(** FIXME: export a better interface in Tactics *) +let delayed_of_tactic tac env sigma = + let _, pv = Proofview.init sigma [] in + let c, pv, _, _ = Proofview.apply env tac pv in + (sigma, c) + +let apply adv ev cb cl = + let map c = None, Loc.tag (delayed_of_tactic c) in + let cb = List.map map cb in + match cl with + | None -> Tactics.apply_with_delayed_bindings_gen adv ev cb + | Some (id, cl) -> Tactics.apply_delayed_in adv ev id cb cl diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli new file mode 100644 index 0000000000..86278f177e --- /dev/null +++ b/src/tac2tactics.mli @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Misctypes +open Tactypes +open Proofview + +(** Local reimplementations of tactics variants from Coq *) + +val apply : advanced_flag -> evars_flag -> + EConstr.constr with_bindings tactic list -> + (Id.t * intro_pattern option) option -> unit tactic |