aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml3
-rw-r--r--tactics/class_tactics.ml23
-rw-r--r--tactics/class_tactics.mli3
-rw-r--r--tactics/eauto.ml7
-rw-r--r--tactics/equality.ml8
-rw-r--r--tactics/redexpr.ml14
-rw-r--r--tactics/tacticals.ml10
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tactics/tactics.ml11
9 files changed, 30 insertions, 51 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f041af1db1..3287c1c354 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -99,8 +99,7 @@ let connect_hint_clenv h gl =
let unify_resolve flags (h : hint) =
Proofview.Goal.enter begin fun gl ->
let clenv, c = connect_hint_clenv h gl in
- let clenv = clenv_unique_resolver ~flags clenv gl in
- Clenvtac.clenv_refine clenv
+ Clenv.res_pf ~flags clenv
end
let unify_resolve_nodelta h = unify_resolve auto_unif_flags h
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 484aab2f00..4156d5f0ee 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -14,7 +14,6 @@
*)
open Pp
-open CErrors
open Util
open Names
open Term
@@ -159,27 +158,17 @@ let e_give_exact flags h =
in
let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
Proofview.Unsafe.tclEVARS sigma <*>
- Clenvtac.unify ~flags t1 <*> exact_no_check c
- end
-
-let clenv_unique_resolver_tac with_evars ~flags clenv' =
- Proofview.Goal.enter begin fun gls ->
- let resolve =
- try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
- with e when noncritical e ->
- let _, info = Exninfo.capture e in
- Proofview.tclZERO ~info e
- in resolve >>= fun clenv' ->
- Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
+ Clenv.unify ~flags t1 <*> exact_no_check c
end
let unify_e_resolve flags = begin fun gls (h, _) ->
let clenv', c = connect_hint_clenv h gls in
- clenv_unique_resolver_tac true ~flags clenv' end
+ Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv'
+ end
let unify_resolve flags = begin fun gls (h, _) ->
let clenv', _ = connect_hint_clenv h gls in
- clenv_unique_resolver_tac false ~flags clenv'
+ Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv'
end
(** Application of a lemma using [refine] instead of the old [w_unify] *)
@@ -446,10 +435,6 @@ let e_possible_resolve db_list local_db secvars only_classes env sigma concl =
let cut_of_hints h =
List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
-let catchable = function
- | Refiner.FailError _ -> true
- | e -> Logic.catchable_exception e [@@ocaml.warning "-3"]
-
let pr_depth l =
let rec fmt elts =
match elts with
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index b97b90d777..381f68f14f 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -15,9 +15,6 @@ open EConstr
val typeclasses_db : string
-val catchable : exn -> bool
-[@@ocaml.deprecated "Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."]
-
val set_typeclasses_debug : bool -> unit
val set_typeclasses_depth : int option -> unit
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 0ff90bc046..d275e15255 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -37,7 +37,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c =
if occur_existential sigma t1 || occur_existential sigma t2 then
Tacticals.New.tclTHENLIST
[Proofview.Unsafe.tclEVARS sigma;
- Clenvtac.unify ~flags t1;
+ Clenv.unify ~flags t1;
exact_no_check c]
else exact_check c
end
@@ -68,10 +68,7 @@ open Auto
let unify_e_resolve flags h =
Proofview.Goal.enter begin fun gl ->
let clenv', c = connect_hint_clenv h gl in
- let clenv' = clenv_unique_resolver ~flags clenv' gl in
- Proofview.tclTHEN
- (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
- (Tactics.Simple.eapply c)
+ Clenv.res_pf ~with_evars:true ~with_classes:true ~flags clenv'
end
let hintmap_of sigma secvars concl =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 79b6dfe920..39017c946f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -154,7 +154,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
let c1 = args.(arglen - 2) in
let c2 = args.(arglen - 1) in
let try_occ (evd', c') =
- Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
+ Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
in
let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
let occs =
@@ -1045,7 +1045,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf ->
let pf_ty = mkArrow eqn Sorts.Relevant false_0 in
let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
- let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
+ let pf = Clenv.clenv_value_cast_meta absurd_clause in
tclTHENS (assert_after Anonymous false_0)
[onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))]
@@ -1067,7 +1067,7 @@ let onEquality with_evars tac (c,lbindc) =
let t = pf_get_type_of gl c in
let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
- let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in
+ let eq_clause' = Clenv.clenv_pose_dependent_evars ~with_evars eq_clause in
let eqn = clenv_type eq_clause' in
(* FIXME evar leak *)
let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in
@@ -1397,7 +1397,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
let pf = applist(congr,[t;resty;injfun;t1;t2]) in
let sigma, pf_typ = Typing.type_of env sigma pf in
let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
- let pf = Clenvtac.clenv_value_cast_meta inj_clause in
+ let pf = Clenv.clenv_value_cast_meta inj_clause in
let ty = simplify_args env sigma (clenv_type inj_clause) in
evdref := sigma;
Some (pf, ty)
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index e000ddce74..c463c06cd5 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -188,8 +188,18 @@ let out_arg = function
| Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
| Locus.ArgArg x -> x
+let out_occurrences occs =
+ let occs = Locusops.occurrences_map (List.map out_arg) occs in
+ match occs with
+ | Locus.OnlyOccurrences (n::_ as nl) when n < 0 ->
+ Locus.AllOccurrencesBut (List.map abs nl)
+ | Locus.OnlyOccurrences nl when List.exists (fun n -> n < 0) nl ->
+ CErrors.user_err Pp.(str "Illegal negative occurrence number.")
+ | Locus.OnlyOccurrences _ | Locus.AllOccurrencesBut _ | Locus.NoOccurrences
+ | Locus.AllOccurrences | Locus.AtLeastOneOccurrence -> occs
+
let out_with_occurrences (occs,c) =
- (Locusops.occurrences_map (List.map out_arg) occs, c)
+ (out_occurrences occs, c)
let e_red f env evm c = evm, f env evm c
@@ -199,7 +209,7 @@ let head_style = false (* Turn to true to have a semantics where simpl
let contextualize f g = function
| Some (occs,c) ->
- let l = Locusops.occurrences_map (List.map out_arg) occs in
+ let l = out_occurrences occs in
let b,c,h = match c with
| Inl r -> true,PRef (global_of_evaluable_reference r),f
| Inr c -> false,c,f in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index a4d306c497..22c5bbe73f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -140,9 +140,7 @@ let ifOnHyp pred tac1 tac2 id gl =
type branch_args = {
ity : pinductive; (* the type we were eliminating on *)
- largs : constr list; (* its arguments *)
branchnum : int; (* the branch number *)
- pred : constr; (* the predicate we used *)
nassums : int; (* number of assumptions/letin to be introduced *)
branchsign : bool list; (* the signature of the branch.
true=assumption, false=let-in *)
@@ -686,22 +684,18 @@ module New = struct
| None -> elimclause'
| Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
in
- let clenv' = clenv_unique_resolver ~flags elimclause' gl in
let after_tac i =
- let (hd,largs) = decompose_app clenv'.evd clenv'.templtyp.Evd.rebus in
let ba = { branchsign = branchsigns.(i);
branchnames = brnames.(i);
nassums = List.length branchsigns.(i);
branchnum = i+1;
- ity = ind;
- largs = List.map (clenv_nf_meta clenv') largs;
- pred = clenv_nf_meta clenv' hd }
+ ity = ind; }
in
tac ba
in
let branchtacs = List.init (Array.length branchsigns) after_tac in
Proofview.tclTHEN
- (Clenvtac.clenv_refine clenv')
+ (Clenv.res_pf ~flags elimclause')
(Proofview.tclEXTEND [] tclIDTAC branchtacs)
end) end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index eebe702259..88419af836 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -89,9 +89,7 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic
type branch_args = private {
ity : pinductive; (** the type we were eliminating on *)
- largs : constr list; (** its arguments *)
branchnum : int; (** the branch number *)
- pred : constr; (** the predicate we used *)
nassums : int; (** number of assumptions/letin to be introduced *)
branchsign : bool list; (** the signature of the branch.
true=assumption, false=let-in *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 65f79b6a51..3133f9be1e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1373,7 +1373,7 @@ let do_replace id = function
[id] is replaced by P using the proof given by [tac] *)
let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac =
- let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
+ let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in
let clenv =
{ clenv with evd = Typeclasses.resolve_typeclasses
~fail:(not with_evars) clenv.env clenv.evd }
@@ -1475,7 +1475,7 @@ let general_elim_clause with_evars flags where indclause elim =
match where with
| None ->
let elimclause = clenv_fchain ~flags indmv elimclause indclause in
- Clenvtac.res_pf elimclause ~with_evars ~with_classes:true ~flags
+ Clenv.res_pf elimclause ~with_evars ~with_classes:true ~flags
| Some id ->
let hypmv =
match List.remove Int.equal indmv (clenv_independent elimclause) with
@@ -1737,7 +1737,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
let n = nb_prod_modulo_zeta sigma thm_ty - nprod in
if n<0 then error "Applied theorem does not have enough premises.";
let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
- Clenvtac.res_pf clause ~with_evars ~flags
+ Clenv.res_pf clause ~with_evars ~flags
with exn when noncritical exn ->
let exn, info = Exninfo.capture exn in
Proofview.tclZERO ~info exn
@@ -4371,8 +4371,7 @@ let induction_tac with_evars params indvars elim =
(* elimclause' is built from elimclause by instantiating all args and params. *)
let elimclause' = recolle_clenv i params indvars elimclause gl in
(* one last resolution (useless?) *)
- let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
- Clenvtac.clenv_refine ~with_evars resolved
+ Clenv.res_pf ~with_evars ~flags:(elim_flags ()) elimclause'
end
(* Apply induction "in place" taking into account dependent
@@ -4813,7 +4812,7 @@ let elim_scheme_type elim t =
(* t is inductive, then CUMUL or CONV is irrelevant *)
clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t
(clenv_meta_type clause mv) clause in
- Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
+ Clenv.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
| _ -> anomaly (Pp.str "elim_scheme_type.")
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 02:08:17 +0000