diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml4 | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/g_class.ml4 | 2 | ||||
| -rw-r--r-- | tactics/g_eqdecide.ml4 | 2 | ||||
| -rw-r--r-- | tactics/g_rewrite.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tacenv.ml | 25 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 2 |
7 files changed, 27 insertions, 10 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 96258a84bc..4674bd030c 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -28,6 +28,8 @@ open Misctypes open Locus open Locusops +DECLARE PLUGIN "eauto" + let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state } let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e87c665d09..f6483e2b3d 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -22,6 +22,8 @@ open Evd open Equality open Misctypes +DECLARE PLUGIN "extratactics" + (**********************************************************************) (* admit, replace, discriminate, injection, simplify_eq *) (* cutrewrite, dependent rewrite *) diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4 index 6012088f7b..1e666e5a55 100644 --- a/tactics/g_class.ml4 +++ b/tactics/g_class.ml4 @@ -11,6 +11,8 @@ open Misctypes open Class_tactics +DECLARE PLUGIN "g_class" + TACTIC EXTEND progress_evars [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.eval_tactic t) ] END diff --git a/tactics/g_eqdecide.ml4 b/tactics/g_eqdecide.ml4 index c9d876d92f..819bbdc518 100644 --- a/tactics/g_eqdecide.ml4 +++ b/tactics/g_eqdecide.ml4 @@ -16,6 +16,8 @@ open Eqdecide +DECLARE PLUGIN "g_eqdecide" + TACTIC EXTEND decide_equality | [ "decide" "equality" ] -> [ decideEqualityGoal ] END diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 779070f80a..27233ea57b 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -21,6 +21,8 @@ open Tacmach open Tacticals open Rewrite +DECLARE PLUGIN "g_rewrite" + type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 9bd3128546..9259048260 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -59,19 +59,18 @@ let () = (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) -let atomic_mactab = ref Id.Map.empty -let register_atomic_ltac id tac = - atomic_mactab := Id.Map.add id tac !atomic_mactab - -let _ = +let initial_atomic = let open Locus in let open Misctypes in let open Genredexpr in let dloc = Loc.ghost in let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in - List.iter - (fun (s,t) -> register_atomic_ltac (Id.of_string s) (TacAtom(dloc,t))) + let fold accu (s, t) = + let body = TacAtom (dloc, t) in + Id.Map.add (Id.of_string s) body accu + in + let ans = List.fold_left fold Id.Map.empty [ "red", TacReduce(Red false,nocl); "hnf", TacReduce(Hnf,nocl); "simpl", TacReduce(Simpl None,nocl); @@ -92,14 +91,20 @@ let _ = "econstructor", TacAnyConstructor (true,None); "reflexivity", TacReflexivity; "symmetry", TacSymmetry nocl - ]; - List.iter - (fun (s,t) -> register_atomic_ltac (Id.of_string s) t) + ] + in + let fold accu (s, t) = Id.Map.add (Id.of_string s) t accu in + List.fold_left fold ans [ "idtac",TacId []; "fail", TacFail(ArgArg 0,[]); "fresh", TacArg(dloc,TacFreshId []) ] +let atomic_mactab = Summary.ref ~name:"atomic_tactics" initial_atomic + +let register_atomic_ltac id tac = + atomic_mactab := Id.Map.add id tac !atomic_mactab + let interp_atomic_ltac id = Id.Map.find id !atomic_mactab let is_primitive_ltac_ident id = diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 8d3d335102..2d9b4da967 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -20,6 +20,8 @@ open Tactics open Errors open Util +DECLARE PLUGIN "tauto" + let assoc_var s ist = let v = Id.Map.find (Names.Id.of_string s) ist.lfun in match Value.to_constr v with |