aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml27
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/hints.ml67
-rw-r--r--tactics/hints.mli1
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tactics.ml38
-rw-r--r--tactics/term_dnet.mli2
7 files changed, 78 insertions, 63 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 998efdd6da..c105116ff9 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -649,17 +649,6 @@ module Search = struct
Evd.add sigma gl evi')
sigma goals
- let fail_if_nonclass info =
- Proofview.Goal.enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
- if is_class_type sigma (Proofview.Goal.concl gl) then
- Proofview.tclUNIT ()
- else (if !typeclasses_debug > 1 then
- Feedback.msg_debug (pr_depth info.search_depth ++
- str": failure due to non-class subgoal " ++
- pr_ev sigma (Proofview.Goal.goal gl));
- Proofview.tclZERO NoApplicableEx) end
-
(** The general hint application tactic.
tac1 + tac2 .... The choice of OR or ORELSE is determined
depending on the dependencies of the goal and the unique/Prop
@@ -798,13 +787,8 @@ module Search = struct
in
if path_matches derivs [] then aux e tl
else
- let filter =
- if false (* in 8.6, still allow non-class subgoals
- info.search_only_classes *) then fail_if_nonclass info
- else Proofview.tclUNIT ()
- in
ortac
- (with_shelf (tac <*> filter) >>= fun s ->
+ (with_shelf tac >>= fun s ->
let i = !idx in incr idx; result s i None)
(fun e' ->
if CErrors.noncritical (fst e') then
@@ -868,12 +852,9 @@ module Search = struct
let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
unit Proofview.tactic =
let open Proofview in
- if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
- Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
- else
- let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
- let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
- search_tac hints depth 1 info
+ let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
+ let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
+ search_tac hints depth 1 info
let search_tac ?(st=full_transparent_state) only_classes dep hints depth =
let open Proofview in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f9e06391a3..d7e697aed2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1808,9 +1808,9 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
match EConstr.kind sigma x, EConstr.kind sigma y with
- | Var x', _ when not (dependent sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
+ | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) ->
subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
- | _, Var y' when not (dependent sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
+ | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) ->
subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
| _ ->
Proofview.tclUNIT ()
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e32807f4b8..d49c8aaa56 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -167,6 +167,7 @@ type hint_mode =
type hints_expr =
| HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+ | HintsResolveIFF of bool * reference list * int option
| HintsImmediate of reference_or_constr list
| HintsUnfold of reference list
| HintsTransparency of reference list * bool
@@ -294,15 +295,15 @@ let strip_params env sigma c =
| App (f, args) ->
(match EConstr.kind sigma f with
| Const (p,_) ->
- let cb = lookup_constant p env in
- (match cb.Declarations.const_proj with
- | Some pb ->
- let n = pb.Declarations.proj_npars in
- if Array.length args > n then
- mkApp (mkProj (Projection.make p false, args.(n)),
- Array.sub args (n+1) (Array.length args - (n + 1)))
- else c
- | None -> c)
+ let p = Projection.make p false in
+ (match lookup_projection p env with
+ | pb ->
+ let n = pb.Declarations.proj_npars in
+ if Array.length args > n then
+ mkApp (mkProj (p, args.(n)),
+ Array.sub args (n+1) (Array.length args - (n + 1)))
+ else c
+ | exception Not_found -> c)
| _ -> c)
| _ -> c
@@ -672,7 +673,7 @@ struct
let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l
- let remove_sdl p sdl = List.Smart.filter p sdl
+ let remove_sdl p sdl = List.filter p sdl
let remove_he st p se =
let sl1' = remove_sdl p se.sentry_nopat in
@@ -684,7 +685,7 @@ struct
let filter (_, h) =
match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
- let hintnopat = List.Smart.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
+ let hintnopat = List.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
{ db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
let remove_one gr db = remove_list [gr] db
@@ -1290,6 +1291,35 @@ let prepare_hint check (poly,local) env init (sigma,c) =
else (Lib.add_anonymous_leaf (input_context_set diff);
IsConstr (c', Univ.ContextSet.empty))
+let project_hint ~poly pri l2r r =
+ let open EConstr in
+ let open Coqlib in
+ let gr = Smartlocate.global_with_alias r in
+ let env = Global.env() in
+ let sigma = Evd.from_env env in
+ let sigma, c = Evd.fresh_global env sigma gr in
+ let t = Retyping.get_type_of env sigma c in
+ let t =
+ Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
+ let sign,ccl = decompose_prod_assum sigma t in
+ let (a,b) = match snd (decompose_app sigma ccl) with
+ | [a;b] -> (a,b)
+ | _ -> assert false in
+ let p =
+ if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
+ let sigma, p = Evd.fresh_global env sigma p in
+ let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
+ let c = it_mkLambda_or_LetIn
+ (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
+ let id =
+ Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
+ in
+ let ctx = Evd.const_univ_entry ~poly sigma in
+ let c = EConstr.to_constr sigma c in
+ let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
+ let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
+ (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c))
+
let interp_hints poly =
fun h ->
let env = Global.env () in
@@ -1319,6 +1349,8 @@ let interp_hints poly =
in
match h with
| HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
+ | HintsResolveIFF (l2r, lc, n) ->
+ HintsResolveEntry (List.map (project_hint ~poly n l2r) lc)
| HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
| HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
| HintsTransparency (lhints, b) ->
@@ -1379,12 +1411,10 @@ let expand_constructor_hints env sigma lems =
(* builds a hint database from a constr signature *)
(* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
-let add_hint_lemmas env sigma eapply lems hint_db =
+let constructor_hints env sigma eapply lems =
let lems = expand_constructor_hints env sigma lems in
- let hintlist' =
- List.map_append (fun (poly, lem) ->
- make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in
- Hint_db.add_list env sigma hintlist' hint_db
+ List.map_append (fun (poly, lem) ->
+ make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems
let make_local_hint_db env sigma ts eapply lems =
let map c = c env sigma in
@@ -1395,8 +1425,9 @@ let make_local_hint_db env sigma ts eapply lems =
| Some ts -> ts
in
let hintlist = List.map_append (make_resolve_hyp env sigma) sign in
- add_hint_lemmas env sigma eapply lems
- (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false))
+ Hint_db.empty ts false
+ |> Hint_db.add_list env sigma hintlist
+ |> Hint_db.add_list env sigma (constructor_hints env sigma eapply lems)
let make_local_hint_db env sigma ?ts eapply lems =
make_local_hint_db env sigma ts eapply lems
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 7ef7f01858..e958f986e2 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -83,6 +83,7 @@ type hint_mode =
type hints_expr =
| HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+ | HintsResolveIFF of bool * Libnames.reference list * int option
| HintsImmediate of reference_or_constr list
| HintsUnfold of Libnames.reference list
| HintsTransparency of Libnames.reference list * bool
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 28cfd57a2d..339abbc2e8 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -469,7 +469,7 @@ let raw_inversion inv_kind id status names =
make_inv_predicate env evdref indf realargs id status concl in
let sigma = !evdref in
let (cut_concl,case_tac) =
- if status != NoDep && (dependent sigma c concl) then
+ if status != NoDep && (local_occur_var sigma id concl) then
Reductionops.beta_applist sigma (elim_predicate, realargs@[c]),
case_then_using
else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 58c62af85a..d7888f6ca2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -158,9 +158,9 @@ let convert_concl ?(check=true) ty k =
let sigma =
if check then begin
ignore (Typing.unsafe_type_of env sigma ty);
- let sigma,b = Reductionops.infer_conv env sigma ty conclty in
- if not b then error "Not convertible.";
- sigma
+ match Reductionops.infer_conv env sigma ty conclty with
+ | None -> error "Not convertible."
+ | Some sigma -> sigma
end else sigma in
let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
@@ -186,11 +186,10 @@ let convert_hyp_no_check = convert_hyp ~check:false
let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
- try
- let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in
- if b then Proofview.Unsafe.tclEVARS sigma
- else Tacticals.New.tclFAIL 0 (str "Not convertible")
- with (* Reduction.NotConvertible *) _ ->
+ match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
+ | Some sigma -> Proofview.Unsafe.tclEVARS sigma
+ | None -> Tacticals.New.tclFAIL 0 (str "Not convertible")
+ | exception _ ->
(** FIXME: Sometimes an anomaly is raised from conversion *)
Tacticals.New.tclFAIL 0 (str "Not convertible")
end
@@ -796,15 +795,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
let t2 = Retyping.get_type_of env sigma origc in
let sigma, t2 = Evarsolve.refresh_universes
~onlyalg:true (Some false) env sigma t2 in
- let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in
- if not b then
+ match infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 with
+ | None ->
if
isSort sigma (whd_all env sigma t1) &&
isSort sigma (whd_all env sigma t2)
then (mayneedglobalcheck := true; sigma)
else
user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.")
- else sigma
+ | Some sigma -> sigma
end
else
if not (isSort sigma (whd_all env sigma t1)) then
@@ -815,9 +814,9 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
let (sigma, t') = t sigma in
let sigma = check_types env sigma mayneedglobalcheck deep t' c in
- let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
- if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
- (sigma, t')
+ match infer_conv ~pb:cv_pb env sigma t' c with
+ | None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
+ | Some sigma -> (sigma, t')
(* Use cumulativity only if changing the conclusion not a subterm *)
let change_on_subterm cv_pb deep t where env sigma c =
@@ -1934,16 +1933,19 @@ let assumption =
let t = NamedDecl.get_type decl in
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
- let (sigma, is_same_type) =
- if only_eq then (sigma, EConstr.eq_constr sigma t concl)
+ let ans =
+ if only_eq then
+ if EConstr.eq_constr sigma t concl then Some sigma
+ else None
else
let env = Proofview.Goal.env gl in
infer_conv env sigma t concl
in
- if is_same_type then
+ match ans with
+ | Some sigma ->
(Proofview.Unsafe.tclEVARS sigma) <*>
exact_no_check (mkVar (NamedDecl.get_id decl))
- else arec gl only_eq rest
+ | None -> arec gl only_eq rest
in
let assumption_tac gl =
let hyps = Proofview.Goal.hyps gl in
diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli
index 2c748f9c93..7bce577899 100644
--- a/tactics/term_dnet.mli
+++ b/tactics/term_dnet.mli
@@ -26,7 +26,7 @@ open Mod_subst
The results returned here are perfect, since post-filtering is done
inside here.
- See lib/dnet.mli for more details.
+ See tactics/dnet.mli for more details.
*)
(** Identifiers to store (right hand side of the association) *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 00:42:14 +0000