aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/autorewrite.ml22
-rw-r--r--tactics/class_tactics.ml5
-rw-r--r--tactics/eqschemes.ml11
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/hints.ml32
-rw-r--r--tactics/hints.mli1
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/leminv.ml5
-rw-r--r--tactics/tactics.ml83
9 files changed, 109 insertions, 58 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 0b0e629ab5..c8fd0b7a75 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -228,7 +228,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
if metas then eqclause
else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
in
- let (equiv, args) = decompose_app (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
+ let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z ->
@@ -236,17 +236,19 @@ let decompose_applied_relation metas env sigma c ctype left2right =
| _ -> raise Not_found
in
try
- let others,(c1,c2) = split_last_two args in
- let ty1, ty2 =
- Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2)
- in
- let ty = EConstr.Unsafe.to_constr ty in
- let ty1 = EConstr.Unsafe.to_constr ty1 in
+ let others,(c1,c2) = split_last_two args in
+ let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in
+ (* XXX: It looks like mk_clenv_from_env should be fixed instead? *)
+ let open EConstr in
+ let hyp_ty = Unsafe.to_constr ty in
+ let hyp_car = Unsafe.to_constr ty1 in
+ let hyp_prf = Unsafe.to_constr @@ Clenv.clenv_value eqclause in
+ let hyp_rel = Unsafe.to_constr @@ mkApp (equiv, Array.of_list others) in
+ let hyp_left = Unsafe.to_constr @@ c1 in
+ let hyp_right = Unsafe.to_constr @@ c2 in
(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
(* else *)
- Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty;
- hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others);
- hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; }
+ Some { hyp_cl=eqclause; hyp_prf; hyp_ty; hyp_car; hyp_rel; hyp_l2r=left2right; hyp_left; hyp_right; }
with Not_found -> None
in
match find_rel ctype with
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c105116ff9..4beeaaae05 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1206,8 +1206,11 @@ let is_ground c =
let autoapply c i =
let open Proofview.Notations in
Proofview.Goal.enter begin fun gl ->
+ let hintdb = try Hints.searchtable_map i with Not_found ->
+ CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ "."))
+ in
let flags = auto_unif_flags Evar.Set.empty
- (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
+ (Hints.Hint_db.transparent_state hintdb) in
let cty = Tacmach.New.pf_unsafe_type_of gl c in
let ce = mk_clenv_from gl (c,cty) in
unify_e_resolve false flags gl
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index eede133291..ad5239116a 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -108,9 +108,14 @@ let get_coq_eq ctx =
user_err Pp.(str "eq not found.")
let univ_of_eq env eq =
- let eq = EConstr.of_constr eq in
- match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) eq)) with
- | Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false)
+ let open EConstr in
+ let eq = of_constr eq in
+ let sigma = Evd.from_env env in
+ match kind sigma (Retyping.get_type_of env sigma eq) with
+ | Prod (_,t,_) -> (match kind sigma t with
+ Sort k ->
+ (match ESorts.kind sigma k with Type u -> u | _ -> assert false)
+ | _ -> assert false)
| _ -> assert false
(**********************************************************************)
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 4b77418ff4..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
@@ -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) ->
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..102b8e54d1 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -293,7 +293,7 @@ let error_too_many_names pats =
str "Unexpected " ++
str (String.plural (List.length pats) "introduction pattern") ++
str ": " ++ pr_enum (Miscprint.pr_intro_pattern
- (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env (Evd.from_env env)))))) pats ++
+ (fun c -> Printer.pr_econstr_env env sigma (snd (c env (Evd.from_env env))))) pats ++
str ".")
let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with
@@ -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/leminv.ml b/tactics/leminv.ml
index f47e6b2cd9..10937322e7 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,9 +232,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let c = fill_holes pfterm in
(* warning: side-effect on ownSign *)
let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
- let invProof = EConstr.Unsafe.to_constr invProof in
- let p = Evarutil.nf_evars_universes sigma invProof in
- p, sigma
+ let p = EConstr.to_constr sigma invProof in
+ p, sigma
let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 58c62af85a..b571b347d3 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 =
@@ -1638,13 +1637,11 @@ let tclORELSEOPT t k =
Proofview.tclZERO ~info e
| Some tac -> tac)
-let general_apply with_delta with_destruct with_evars clear_flag
- {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} =
+let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
+ clear_flag {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
- let flags =
- if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
(* The actual type of the theorem. It will be matched against the
goal. If this fails, then the head constant will be unfolded step by
step. *)
@@ -1653,7 +1650,12 @@ let general_apply with_delta with_destruct with_evars clear_flag
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
-
+ let ts =
+ if respect_opaque then Conv_oracle.get_transp_state (oracle env)
+ else full_transparent_state
+ in
+ let flags =
+ if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
let thm_ty0 = nf_betaiota env sigma (Retyping.get_type_of env sigma c) in
let try_apply thm_ty nprod =
try
@@ -1719,14 +1721,14 @@ let rec apply_with_bindings_gen b e = function
(general_apply b b e k cb)
(apply_with_bindings_gen b e cbl)
-let apply_with_delayed_bindings_gen b e l =
+let apply_with_delayed_bindings_gen b e l =
let one k {CAst.loc;v=f} =
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let (sigma, cb) = f env sigma in
Tacticals.New.tclWITHHOLES e
- (general_apply b b e k CAst.(make ?loc cb)) sigma
+ (general_apply ~respect_opaque:(not b) b b e k CAst.(make ?loc cb)) sigma
end
in
let rec aux = function
@@ -1801,14 +1803,12 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
in
aux (make_clenv_binding env sigma (d,thm) lbind)
-let apply_in_once sidecond_first with_delta with_destruct with_evars naming
- id (clear_flag,{ CAst.loc; v= d,lbind}) tac =
+let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
+ with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac =
let open Context.Rel.Declaration in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
- let flags =
- if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
let t' = Tacmach.New.pf_get_hyp_typ id gl in
let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in
@@ -1816,6 +1816,12 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
+ let ts =
+ if respect_opaque then Conv_oracle.get_transp_state (oracle env)
+ else full_transparent_state
+ in
+ let flags =
+ if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
try
let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in
clenv_refine_in ~sidecond_first with_evars targetid id sigma clause
@@ -1835,14 +1841,14 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
aux [] with_destruct d
end
-let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming
- id (clear_flag,{CAst.loc;v=f}) tac =
+let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta
+ with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let (sigma, c) = f env sigma in
Tacticals.New.tclWITHHOLES with_evars
- (apply_in_once sidecond_first with_delta with_destruct with_evars
+ (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars
naming id (clear_flag,CAst.(make ?loc c)) tac)
sigma
end
@@ -1934,16 +1940,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
@@ -2529,11 +2538,11 @@ let assert_as first hd ipat t =
(* apply in as *)
-let general_apply_in sidecond_first with_delta with_destruct with_evars
- id lemmas ipat =
+let general_apply_in ?(respect_opaque=false) sidecond_first with_delta
+ with_destruct with_evars id lemmas ipat =
let tac (naming,lemma) tac id =
- apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
- naming id lemma tac in
+ apply_in_delayed_once ~respect_opaque sidecond_first with_delta
+ with_destruct with_evars naming id lemma tac in
Proofview.Goal.enter begin fun gl ->
let destopt =
if with_evars then MoveLast (* evars would depend on the whole context *)
@@ -2564,7 +2573,7 @@ let apply_in simple with_evars id lemmas ipat =
general_apply_in false simple simple with_evars id lemmas ipat
let apply_delayed_in simple with_evars id lemmas ipat =
- general_apply_in false simple simple with_evars id lemmas ipat
+ general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat
(*****************************)
(* Tactics abstracting terms *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 03:29:57 +0000