aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/eauto.ml468
-rw-r--r--tactics/eauto.mli6
-rw-r--r--tactics/tacenv.ml8
-rw-r--r--tactics/tacenv.mli4
-rw-r--r--tactics/tauto.ml42
6 files changed, 52 insertions, 38 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e97a42e6e4..c0fe514f08 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -184,7 +184,7 @@ let with_prods nprods poly (c, clenv) f gls =
let rec e_trivial_fail_db db_list local_db goal =
let tacl =
- Eauto.registered_e_assumption ::
+ Proofview.V82.of_tactic Eauto.registered_e_assumption ::
(tclTHEN (Proofview.V82.of_tactic Tactics.intro)
(function g'->
let d = pf_last_hyp g' in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 3d98bc6e19..789bcd1bdd 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -33,27 +33,35 @@ DECLARE PLUGIN "eauto"
let eauto_unif_flags = auto_flags_of_state 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
+let e_give_exact ?(flags=eauto_unif_flags) c =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let t1 = Tacmach.New.pf_type_of gl c in
+ let t2 = Tacmach.New.pf_concl gl in
if occur_existential t1 || occur_existential t2 then
- tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
- else Proofview.V82.of_tactic (exact_check c) gl
+ Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c))
+ else exact_check c
+ end
let assumption id = e_give_exact (mkVar id)
-let e_assumption gl =
- tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
+let e_assumption =
+ Proofview.Goal.enter begin fun gl ->
+ Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl))
+ end
TACTIC EXTEND eassumption
-| [ "eassumption" ] -> [ Proofview.V82.tactic e_assumption ]
+| [ "eassumption" ] -> [ e_assumption ]
END
TACTIC EXTEND eexact
-| [ "eexact" constr(c) ] -> [ Proofview.V82.tactic (e_give_exact c) ]
+| [ "eexact" constr(c) ] -> [ e_give_exact c ]
END
-let registered_e_assumption gl =
- tclFIRST (List.map (fun id gl -> e_give_exact (mkVar id) gl)
- (pf_ids_of_hyps gl)) gl
+let registered_e_assumption =
+ Proofview.Goal.enter begin fun gl ->
+ Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id))
+ (Tacmach.New.pf_ids_of_hyps gl))
+ end
(************************************************************************)
(* PROLOG tactic *)
@@ -82,7 +90,7 @@ let one_step l gl =
[Proofview.V82.of_tactic Tactics.intro]
@ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
@ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
- @ (List.map assumption (pf_ids_of_hyps gl))
+ @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl))
let rec prolog l n gl =
if n <= 0 then error "prolog - failure";
@@ -138,19 +146,21 @@ let e_exact poly flags (c,clenv) =
if poly then Clenv.refresh_undefined_univs clenv
else clenv, Univ.empty_level_subst
in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c)
-
-let rec e_trivial_fail_db db_list local_db goal =
+
+let rec e_trivial_fail_db db_list local_db =
+ let next = Proofview.Goal.nf_enter begin fun gl ->
+ let d = Tacmach.New.pf_last_hyp gl in
+ let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) d in
+ e_trivial_fail_db db_list (Hint_db.add_list hintl local_db)
+ end in
+ Proofview.Goal.enter begin fun gl ->
let tacl =
registered_e_assumption ::
- (tclTHEN (Proofview.V82.of_tactic Tactics.intro)
- (function g'->
- let d = pf_last_hyp g' in
- let hintl = make_resolve_hyp (pf_env g') (project g') d in
- (e_trivial_fail_db db_list
- (Hint_db.add_list hintl local_db) g'))) ::
- (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
+ (Tacticals.New.tclTHEN Tactics.intro next) ::
+ (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl)))
in
- tclFIRST (List.map tclCOMPLETE tacl) goal
+ Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
+ end
and e_my_find_search db_list local_db hdc concl =
let hint_of_db = hintmap_of hdc concl in
@@ -164,14 +174,14 @@ and e_my_find_search db_list local_db hdc concl =
(b,
let tac =
match t with
- | Res_pf (term,cl) -> Proofview.V82.of_tactic (unify_resolve poly st (term,cl))
- | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
+ | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
+ | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl))
| Give_exact (c,cl) -> e_exact poly st (c,cl)
| Res_pf_THEN_trivial_fail (term,cl) ->
- tclTHEN (unify_e_resolve poly st (term,cl))
- (e_trivial_fail_db db_list local_db)
- | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
- | Extern tacast -> Proofview.V82.of_tactic (conclPattern concl p tacast)
+ (Tacticals.New.tclTHEN (Proofview.V82.tactic (unify_e_resolve poly st (term,cl)))
+ (e_trivial_fail_db db_list local_db))
+ | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl)
+ | Extern tacast -> conclPattern concl p tacast
in
(tac,lazy (pr_autotactic t)))
in
@@ -223,7 +233,7 @@ module SearchProblem = struct
| [] -> []
| (tac,pptac) :: tacl ->
try
- let lgls = apply_tac_list tac glls in
+ let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in
(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
(lgls,pptac) :: aux tacl
@@ -272,7 +282,7 @@ module SearchProblem = struct
{ depth = s.depth; tacres = res;
last_tactic = pp; dblist = s.dblist;
localdb = ldb :: List.tl s.localdb; prev = ps })
- (filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro,lazy (str "intro")])
+ (filter_tactics s.tacres [Tactics.intro,lazy (str "intro")])
in
let rec_tacs =
let l =
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 7073e8a2b8..b55c70fa12 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -21,11 +21,11 @@ val wit_auto_using :
Genarg.genarg_type
-val e_assumption : tactic
+val e_assumption : unit Proofview.tactic
-val registered_e_assumption : tactic
+val registered_e_assumption : unit Proofview.tactic
-val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic
+val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic
val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> open_constr list ->
hint_db_name list option -> tactic
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 84c0a99b18..53f3f5652c 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -47,7 +47,7 @@ let pr_tacname t =
let tac_tab = ref MLTacMap.empty
-let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
+let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) =
let () =
if MLTacMap.mem s !tac_tab then
if overwrite then
@@ -58,9 +58,11 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
in
tac_tab := MLTacMap.add s t !tac_tab
-let interp_ml_tactic s =
+let interp_ml_tactic { mltac_name = s; mltac_index = i } =
try
- MLTacMap.find s !tac_tab
+ let tacs = MLTacMap.find s !tac_tab in
+ let () = if Array.length tacs <= i then raise Not_found in
+ tacs.(i)
with Not_found ->
Errors.errorlabstrm ""
(str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.")
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 29677fd4ca..424bb142c7 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -48,8 +48,8 @@ type ml_tactic =
typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic
(** Type of external tactics, used by [TacML]. *)
-val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit
+val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic array -> unit
(** Register an external tactic. *)
-val interp_ml_tactic : ml_tactic_name -> ml_tactic
+val interp_ml_tactic : ml_tactic_entry -> ml_tactic
(** Get the named tactic. Raises a user error if it does not exist. *)
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 4b03ff249f..e6f33a47be 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -159,6 +159,8 @@ let flatten_contravariant_conj flags ist =
let constructor i =
let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in
+ (** Take care of the index: this is the second entry in constructor. *)
+ let name = { Tacexpr.mltac_name = name; mltac_index = 1 } in
let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in
Tacexpr.TacML (Loc.ghost, name, [i])
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 23:33:01 +0000