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.ml464
-rw-r--r--tactics/eauto.mli6
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/tacenv.ml8
-rw-r--r--tactics/tacenv.mli4
-rw-r--r--tactics/tauto.ml42
7 files changed, 51 insertions, 37 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index ef78a953ac..e1fe51656f 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 34f87c6cf0..b7dc7b4931 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_unsafe_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_unsafe_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
@@ -165,14 +175,14 @@ and e_my_find_search db_list local_db hdc concl =
let tac = function
| 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) -> Proofview.V82.tactic (e_exact poly st (c,cl))
+ | Give_exact (c,cl) -> e_exact poly st (c,cl)
| Res_pf_THEN_trivial_fail (term,cl) ->
- Proofview.V82.tactic (tclTHEN (unify_e_resolve poly st (term,cl))
- (e_trivial_fail_db db_list local_db))
+ 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
- let tac = Proofview.V82.of_tactic (run_hint t tac) in
+ let tac = run_hint t tac in
(tac, lazy (pr_hint t)))
in
List.map tac_of_hint hintl
@@ -224,7 +234,7 @@ module SearchProblem = struct
| [] -> []
| (tac, cost, 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, cost, pptac) :: aux tacl
@@ -262,7 +272,7 @@ module SearchProblem = struct
prev = ps}) l
in
let intro_tac =
- let l = filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro, (-1), lazy (str "intro")] in
+ let l = filter_tactics s.tacres [Tactics.intro, (-1), lazy (str "intro")] in
List.map
(fun (lgls, cost, pp) ->
let g' = first_goal lgls in
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/equality.ml b/tactics/equality.ml
index ea74dc37ea..d78ba8c629 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1662,7 +1662,7 @@ let default_subst_tactic_flags () =
else
{ only_leibniz = true; rewrite_dependent_proof = false }
-let regular_subst_tactic = ref false
+let regular_subst_tactic = ref true
let _ =
declare_bool_option
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 09a98bc8cc..c1e4d72e38 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -49,7 +49,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
@@ -60,9 +60,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 " ++ pr_tacname s ++ str " is not installed.")
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 2df6bb04a2..47d9efda57 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -64,8 +64,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 b4c7bffa9c..59c5792377 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-03 13:39:57 +0000