aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml18
-rw-r--r--tactics/eauto.ml6
-rw-r--r--tactics/eqdecide.ml10
-rw-r--r--tactics/equality.ml102
-rw-r--r--tactics/equality.mli2
-rw-r--r--tactics/hipattern.ml47
-rw-r--r--tactics/hipattern.mli18
-rw-r--r--tactics/tactics.ml159
8 files changed, 208 insertions, 154 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 371debede..b98b10315 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1342,7 +1342,7 @@ module Search = struct
| Some i -> str ", with depth limit " ++ int i));
tac
- let run_on_evars p evm tac =
+ let run_on_evars env evm p tac =
match evars_to_goals p evm with
| None -> None (* This happens only because there's no evar having p *)
| Some (goals, evm') ->
@@ -1357,7 +1357,7 @@ module Search = struct
let pv = Proofview.unshelve goals pv in
try
let (), pv', (unsafe, shelved, gaveup), _ =
- Proofview.apply (Global.env ()) tac pv
+ Proofview.apply env tac pv
in
if Proofview.finished pv' then
let evm' = Proofview.return pv' in
@@ -1374,22 +1374,22 @@ module Search = struct
else raise Not_found
with Logic_monad.TacticFailure _ -> raise Not_found
- let evars_eauto depth only_classes unique dep st hints p evd =
+ let evars_eauto env evd depth only_classes unique dep st hints p =
let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
- let res = run_on_evars p evd eauto_tac in
+ let res = run_on_evars env evd p eauto_tac in
match res with
| None -> evd
| Some evd' -> evd'
- let typeclasses_eauto ?depth unique st hints p evd =
- evars_eauto depth true unique false st hints p evd
+ let typeclasses_eauto env evd ?depth unique st hints p =
+ evars_eauto env evd depth true unique false st hints p
(** Typeclasses eauto is an eauto which tries to resolve only
goals of typeclass type, and assumes that the initially selected
evars in evd are independent of the rest of the evars *)
- let typeclasses_resolve debug depth unique p evd =
+ let typeclasses_resolve env evd debug depth unique p =
let db = searchtable_map typeclasses_db in
- typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd
+ typeclasses_eauto env evd ?depth unique (Hint_db.transparent_state db) [db] p
end
(** Binding to either V85 or Search implementations. *)
@@ -1532,7 +1532,7 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
if get_typeclasses_legacy_resolution () then
V85.resolve_all_evars_once debug depth unique p evd
else
- Search.typeclasses_resolve debug depth unique p evd
+ Search.typeclasses_resolve env evd debug depth unique p
in
if has_undefined p oevd evd' then raise Unresolved;
docomp evd' comps
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 65864bd47..2b5bbfcd1 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -86,16 +86,16 @@ let rec prolog l n gl =
let prol = (prolog l (n-1)) in
(tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
-let out_term = function
+let out_term env = function
| IsConstr (c, _) -> c
- | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance (Global.env ()) gr))
+ | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr))
let prolog_tac l n =
Proofview.V82.tactic begin fun gl ->
let map c =
let (sigma, c) = c (pf_env gl) (project gl) in
let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in
- out_term c
+ out_term (pf_env gl) c
in
let l = List.map map l in
try (prolog l n gl)
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index d4cad3fa8..e16fcec7c 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -155,9 +155,9 @@ open Proofview.Notations
(* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *)
-let match_eqdec sigma c =
+let match_eqdec env sigma c =
try
- let (eqonleft,_,c1,c2,ty) = match_eqdec sigma c in
+ let (eqonleft,_,c1,c2,ty) = match_eqdec env sigma c in
let (op,eq1,noteq,eq2) =
match EConstr.kind sigma c with
| App (op,[|ty1;ty2|]) ->
@@ -202,8 +202,9 @@ let solveEqBranch rectype =
begin
Proofview.Goal.enter begin fun gl ->
let concl = pf_concl gl in
+ let env = Proofview.Goal.env gl in
let sigma = project gl in
- match_eqdec sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) ->
+ match_eqdec env sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) ->
let (mib,mip) = Global.lookup_inductive rectype in
let nparams = mib.mind_nparams in
let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in
@@ -229,8 +230,9 @@ let decideGralEquality =
begin
Proofview.Goal.enter begin fun gl ->
let concl = pf_concl gl in
+ let env = Proofview.Goal.env gl in
let sigma = project gl in
- match_eqdec sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) ->
+ match_eqdec env sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) ->
let headtyp = hd_app sigma (pf_compute gl typ) in
begin match EConstr.kind sigma headtyp with
| Ind (mi,_) -> Proofview.tclUNIT mi
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 66345ce43..ad6abfa1f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -334,25 +334,27 @@ let (forward_general_setoid_rewrite_clause, general_setoid_rewrite_clause) = Hoo
(* Do we have a JMeq instance on twice the same domains ? *)
-let jmeq_same_dom gl = function
+let jmeq_same_dom env sigma = function
| None -> true (* already checked in Hipattern.find_eq_data_decompose *)
| Some t ->
- let rels, t = decompose_prod_assum (project gl) t in
- let env = push_rel_context rels (Proofview.Goal.env gl) in
- match decompose_app (project gl) t with
- | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
+ let rels, t = decompose_prod_assum sigma t in
+ let env = push_rel_context rels env in
+ match decompose_app sigma t with
+ | _, [dom1; _; dom2;_] -> is_conv env sigma dom1 dom2
| _ -> false
(* find_elim determines which elimination principle is necessary to
eliminate lbeq on sort_of_gl. *)
-let find_elim hdcncl lft2rgt dep cls ot gl =
+let find_elim hdcncl lft2rgt dep cls ot =
+ Proofview.Goal.enter_one begin fun gl ->
let sigma = project gl in
let is_global gr c = Termops.is_global sigma gr c in
let inccl = Option.is_empty cls in
+ let env = Proofview.Goal.env gl in
if (is_global Coqlib.glob_eq hdcncl ||
(is_global Coqlib.glob_jmeq hdcncl &&
- jmeq_same_dom gl ot)) && not dep
+ jmeq_same_dom env sigma ot)) && not dep
then
let c =
match EConstr.kind sigma hdcncl with
@@ -382,9 +384,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
Logic.eq or Jmeq just before *)
assert false
in
- let (sigma, elim) = fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
- let elim = EConstr.of_constr elim in
- (sigma, (elim, Safe_typing.empty_private_constants))
+ pf_constr_of_global (ConstRef c)
else
let scheme_name = match dep, lft2rgt, inccl with
(* Non dependent case *)
@@ -400,14 +400,12 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
in
match EConstr.kind sigma hdcncl with
| Ind (ind,u) ->
+
let c, eff = find_scheme scheme_name ind in
- (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
- let (sigma, elim) =
- fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
- in
- let elim = EConstr.of_constr elim in
- (sigma, (elim, eff))
+ Proofview.tclEFFECTS eff <*>
+ pf_constr_of_global (ConstRef c)
| _ -> assert false
+ end
let type_of_clause cls gl = match cls with
| None -> Proofview.Goal.concl gl
@@ -420,9 +418,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
let dep_fun = if isatomic then dependent else dependent_no_evar in
let type_of_cls = type_of_clause cls gl in
let dep = dep_proof_ok && dep_fun evd c type_of_cls in
- let (sigma, (elim, effs)) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
- Proofview.Unsafe.tclEVARS sigma <*>
- Proofview.tclEFFECTS effs <*>
+ find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim ->
general_elim_clause with_evars frzevars tac cls c t l
(match lft2rgt with None -> false | Some b -> b)
{elimindex = None; elimbody = (elim,NoBindings); elimrename = None}
@@ -536,7 +532,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
let do_hyps =
(* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
let ids gl =
- let ids_in_c = Termops.global_vars_set (Global.env()) (project gl) (fst c) in
+ let ids_in_c = Termops.global_vars_set (Proofview.Goal.env gl) (project gl) (fst c) in
let ids_of_hyps = pf_ids_of_hyps gl in
Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
in
@@ -858,7 +854,8 @@ let descend_then env sigma head dirn =
let IndType (indf,_) =
try find_rectype env sigma (get_type_of env sigma head)
with Not_found ->
- user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") in
+ user_err Pp.(str "Cannot project on an inductive type derived from a dependency.")
+ in
let indp,_ = (dest_ind_family indf) in
let ind, _ = check_privacy env indp in
let (mib,mip) = lookup_mind_specif env ind in
@@ -880,7 +877,7 @@ let descend_then env sigma head dirn =
List.map build_branch
(List.interval 1 (Array.length mip.mind_consnames)) in
let ci = make_case_info env ind RegularStyle in
- sigma, Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
+ Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
(* Now we need to construct the discriminator, given a discriminable
position. This boils down to:
@@ -925,23 +922,20 @@ let build_selector env sigma dirn c ind special default =
let brl =
List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
let ci = make_case_info env ind RegularStyle in
- sigma, mkCase (ci, p, c, Array.of_list brl)
+ mkCase (ci, p, c, Array.of_list brl)
-let build_coq_False sigma = Evarutil.new_global sigma (build_coq_False ())
-let build_coq_True sigma = Evarutil.new_global sigma (build_coq_True ())
-let build_coq_I sigma = Evarutil.new_global sigma (build_coq_I ())
+let build_coq_False () = pf_constr_of_global (build_coq_False ())
+let build_coq_True () = pf_constr_of_global (build_coq_True ())
+let build_coq_I () = pf_constr_of_global (build_coq_I ())
-let rec build_discriminator env sigma dirn c = function
+let rec build_discriminator env sigma true_0 false_0 dirn c = function
| [] ->
let ind = get_type_of env sigma c in
- let sigma, true_0 = build_coq_True sigma in
- let sigma, false_0 = build_coq_False sigma in
build_selector env sigma dirn c ind true_0 false_0
| ((sp,cnum),argnum)::l ->
- let sigma, false_0 = build_coq_False sigma in
let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
let newc = mkRel(cnum_nlams-argnum) in
- let sigma, subval = build_discriminator cnum_env sigma dirn newc l in
+ let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in
kont sigma subval (false_0,mkSort (Prop Null))
(* Note: discrimination could be more clever: if some elimination is
@@ -984,14 +978,15 @@ let ind_scheme_of_eq lbeq =
ConstRef c, eff
-let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq =
- let sigma, i = build_coq_I sigma in
- let sigma, absurd_term = build_coq_False sigma in
+let discrimination_pf e (t,t1,t2) discriminator lbeq =
+ build_coq_I () >>= fun i ->
+ build_coq_False () >>= fun absurd_term ->
let eq_elim, eff = ind_scheme_of_eq lbeq in
- let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in
- let eq_elim = EConstr.of_constr eq_elim in
- sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
- eff
+ Proofview.tclEFFECTS eff <*>
+ pf_constr_of_global eq_elim >>= fun eq_elim ->
+ Proofview.tclUNIT
+ (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term)
+
let eq_baseid = Id.of_string "e"
@@ -1005,19 +1000,24 @@ let apply_on_clause (f,t) clause =
clenv_fchain ~with_univs:false argmv f_clause clause
let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
+ build_coq_True () >>= fun true_0 ->
+ build_coq_False () >>= fun false_0 ->
let e = next_ident_away eq_baseid (ids_of_context env) in
let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
- let sigma, discriminator =
- build_discriminator e_env sigma dirn (mkVar e) cpath in
- let sigma,(pf, absurd_term), eff =
- discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in
- let pf_ty = mkArrow eqn absurd_term in
- let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
- let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
- Proofview.Unsafe.tclEVARS sigma <*>
- Proofview.tclEFFECTS eff <*>
- tclTHENS (assert_after Anonymous absurd_term)
- [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))]
+ let discriminator =
+ try
+ Proofview.tclUNIT
+ (build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath)
+ with
+ UserError _ as ex -> Proofview.tclZERO ex
+ in
+ discriminator >>= fun discriminator ->
+ discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) ->
+ let pf_ty = mkArrow eqn absurd_term in
+ let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
+ let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
+ tclTHENS (assert_after Anonymous absurd_term)
+ [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))]
let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
@@ -1303,7 +1303,7 @@ let rec build_injrec env sigma dflt c = function
let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
let newc = mkRel(cnum_nlams-argnum) in
let sigma, (subval,tuplety,dfltval) = build_injrec cnum_env sigma dflt newc l in
- let sigma, res = kont sigma subval (dfltval,tuplety) in
+ let res = kont sigma subval (dfltval,tuplety) in
sigma, (res, tuplety,dfltval)
with
UserError _ -> failwith "caught"
@@ -1536,7 +1536,7 @@ let decomp_tuple_term env sigma c t =
let rec decomprec inner_code ex exty =
let iterated_decomp =
try
- let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose sigma ex in
+ let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose env sigma ex in
let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code])
and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in
let cdrtyp = beta_applist sigma (p,[car]) in
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 421f7c7f5..a4d1c0f9b 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -126,4 +126,4 @@ val set_eq_dec_scheme_kind : mutual scheme_kind -> unit
(* [build_selector env sigma i c t u v] matches on [c] of
type [t] and returns [u] in branch [i] and [v] on other branches *)
val build_selector : env -> evar_map -> int -> constr -> types ->
- constr -> constr -> evar_map * constr
+ constr -> constr -> constr
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 4101004d4..b057cf72b 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -280,10 +280,7 @@ let coq_refl_jm_pattern =
open Globnames
-let is_matching sigma x y = is_matching (Global.env ()) sigma x y
-let matches sigma x y = matches (Global.env ()) sigma x y
-
-let match_with_equation sigma t =
+let match_with_equation env sigma t =
if not (isApp sigma t) then raise NoEquationFound;
let (hdapp,args) = destApp sigma t in
match EConstr.kind sigma hdapp with
@@ -302,11 +299,11 @@ let match_with_equation sigma t =
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
if Int.equal nconstr 1 then
- if is_matching sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then
+ if is_matching env sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then
None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
- else if is_matching sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then
+ else if is_matching env sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then
None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if is_matching sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then
+ else if is_matching env sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then
None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
else raise NoEquationFound
else raise NoEquationFound
@@ -335,8 +332,8 @@ let is_equality_type sigma t = op2bool (match_with_equality_type sigma t)
(** X1 -> X2 **)
let coq_arrow_pattern = mkPattern (mkGArrow (mkGPatVar "X1") (mkGPatVar "X2"))
-let match_arrow_pattern sigma t =
- let result = matches sigma coq_arrow_pattern t in
+let match_arrow_pattern env sigma t =
+ let result = matches env sigma coq_arrow_pattern t in
match Id.Map.bindings result with
| [(m1,arg);(m2,mind)] ->
assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
@@ -349,13 +346,13 @@ let match_with_imp_term sigma c =
let is_imp_term sigma c = op2bool (match_with_imp_term sigma c)
-let match_with_nottype sigma t =
+let match_with_nottype env sigma t =
try
- let (arg,mind) = match_arrow_pattern sigma t in
+ let (arg,mind) = match_arrow_pattern env sigma t in
if is_empty_type sigma mind then Some (mind,arg) else None
with PatternMatchingFailure -> None
-let is_nottype sigma t = op2bool (match_with_nottype sigma t)
+let is_nottype env sigma t = op2bool (match_with_nottype env sigma t)
(* Forall *)
@@ -481,7 +478,7 @@ let dest_nf_eq gls eqn =
(*** Sigma-types *)
-let match_sigma sigma ex =
+let match_sigma env sigma ex =
match EConstr.kind sigma ex with
| App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_exist_ref) f ->
build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr)
@@ -489,19 +486,19 @@ let match_sigma sigma ex =
build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr)
| _ -> raise PatternMatchingFailure
-let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
- match_sigma ex
+let find_sigma_data_decompose env ex = (* fails with PatternMatchingFailure *)
+ match_sigma env ex
(* Pattern "(sig ?1 ?2)" *)
let coq_sig_pattern =
lazy (mkPattern (mkGAppRef coq_sig_ref [mkGPatVar "X1"; mkGPatVar "X2"]))
-let match_sigma sigma t =
- match Id.Map.bindings (matches sigma (Lazy.force coq_sig_pattern) t) with
+let match_sigma env sigma t =
+ match Id.Map.bindings (matches env sigma (Lazy.force coq_sig_pattern) t) with
| [(_,a); (_,p)] -> (a,p)
| _ -> anomaly (Pp.str "Unexpected pattern.")
-let is_matching_sigma sigma t = is_matching sigma (Lazy.force coq_sig_pattern) t
+let is_matching_sigma env sigma t = is_matching env sigma (Lazy.force coq_sig_pattern) t
(*** Decidable equalities *)
@@ -533,15 +530,15 @@ let coq_eqdec_rev_pattern = coq_eqdec ~sum:coq_or_ref ~rev:true
let op_or = coq_or_ref
let op_sum = coq_sumbool_ref
-let match_eqdec sigma t =
+let match_eqdec env sigma t =
let eqonleft,op,subst =
- try true,op_sum,matches sigma (Lazy.force coq_eqdec_inf_pattern) t
+ try true,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_pattern) t
with PatternMatchingFailure ->
- try false,op_sum,matches sigma (Lazy.force coq_eqdec_inf_rev_pattern) t
+ try false,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_rev_pattern) t
with PatternMatchingFailure ->
- try true,op_or,matches sigma (Lazy.force coq_eqdec_pattern) t
+ try true,op_or,matches env sigma (Lazy.force coq_eqdec_pattern) t
with PatternMatchingFailure ->
- false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in
+ false,op_or,matches env sigma (Lazy.force coq_eqdec_rev_pattern) t in
match Id.Map.bindings subst with
| [(_,typ);(_,c1);(_,c2)] ->
eqonleft, Lazy.force op, c1, c2, typ
@@ -551,8 +548,8 @@ let match_eqdec sigma t =
let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole]))
let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef coq_False_ref)))
-let is_matching_not sigma t = is_matching sigma (Lazy.force coq_not_pattern) t
-let is_matching_imp_False sigma t = is_matching sigma (Lazy.force coq_imp_False_pattern) t
+let is_matching_not env sigma t = is_matching env sigma (Lazy.force coq_not_pattern) t
+let is_matching_imp_False env sigma t = is_matching env sigma (Lazy.force coq_imp_False_pattern) t
(* Remark: patterns that have references to the standard library must
be evaluated lazily (i.e. at the time they are used, not a the time
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 59406e158..8ff6fe95c 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -81,8 +81,8 @@ val is_inductive_equality : inductive -> bool
val match_with_equality_type : (constr * constr list) matching_function
val is_equality_type : testing_function
-val match_with_nottype : (constr * constr) matching_function
-val is_nottype : testing_function
+val match_with_nottype : Environ.env -> (constr * constr) matching_function
+val is_nottype : Environ.env -> testing_function
val match_with_forall_term : (Name.t * constr * constr) matching_function
val is_forall_term : testing_function
@@ -114,7 +114,7 @@ type equation_kind =
exception NoEquationFound
val match_with_equation:
- evar_map -> constr -> coq_eq_data option * constr * equation_kind
+ Environ.env -> evar_map -> constr -> coq_eq_data option * constr * equation_kind
(***** Destructing patterns bound to some theory *)
@@ -132,21 +132,21 @@ val find_eq_data : evar_map -> constr -> coq_eq_data * EInstance.t * equation_ki
(** Match a term of the form [(existT A P t p)]
Returns associated lemmas and [A,P,t,p] *)
-val find_sigma_data_decompose : evar_map -> constr ->
+val find_sigma_data_decompose : Environ.env -> evar_map -> constr ->
coq_sigma_data * (EInstance.t * constr * constr * constr * constr)
(** Match a term of the form [{x:A|P}], returns [A] and [P] *)
-val match_sigma : evar_map -> constr -> constr * constr
+val match_sigma : Environ.env -> evar_map -> constr -> constr * constr
-val is_matching_sigma : evar_map -> constr -> bool
+val is_matching_sigma : Environ.env -> evar_map -> constr -> bool
(** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
[t,u,T] and a boolean telling if equality is on the left side *)
-val match_eqdec : evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
+val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr)
(** Match a negation *)
-val is_matching_not : evar_map -> constr -> bool
-val is_matching_imp_False : evar_map -> constr -> bool
+val is_matching_not : Environ.env -> evar_map -> constr -> bool
+val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 82d58074b..67bc55d3f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -436,19 +436,85 @@ let find_name mayrepl decl naming gl = match naming with
id
(**************************************************************)
+(* Computing position of hypotheses for replacing *)
+(**************************************************************)
+
+let get_next_hyp_position id =
+ let rec aux = function
+ | [] -> error_no_such_hypothesis id
+ | decl :: right ->
+ if Id.equal (NamedDecl.get_id decl) id then
+ match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveFirst
+ else
+ aux right
+ in
+ aux
+
+let get_previous_hyp_position id =
+ let rec aux dest = function
+ | [] -> error_no_such_hypothesis id
+ | decl :: right ->
+ let hyp = NamedDecl.get_id decl in
+ if Id.equal hyp id then dest else aux (MoveAfter hyp) right
+ in
+ aux MoveLast
+
+(**************************************************************)
(* Cut rule *)
(**************************************************************)
+let clear_hyps2 env sigma ids sign t cl =
+ try
+ let evdref = ref (Evd.clear_metas sigma) in
+ let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
+ (hyps, t, cl, !evdref)
+ with Evarutil.ClearDependencyError (id,err) ->
+ error_replacing_dependency env sigma id err
+
+let internal_cut_gen ?(check=true) dir replace id t =
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Tacmach.New.project gl in
+ let concl = Proofview.Goal.concl gl in
+ let store = Proofview.Goal.extra gl in
+ let sign = named_context_val env in
+ let sign',t,concl,sigma =
+ if replace then
+ let nexthyp = get_next_hyp_position id (named_context_of_val sign) in
+ let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
+ let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in
+ sign',t,concl,sigma
+ else
+ (if check && mem_named_context_val id sign then
+ user_err (str "Variable " ++ pr_id id ++ str " is already declared.");
+ push_named_context_val (LocalAssum (id,t)) sign,t,concl,sigma) in
+ let nf_t = nf_betaiota sigma t in
+ Proofview.tclTHEN
+ (Proofview.Unsafe.tclEVARS sigma)
+ (Refine.refine ~typecheck:false begin fun sigma ->
+ let (sigma,ev,ev') =
+ if dir then
+ let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
+ let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+ (sigma,ev,ev')
+ else
+ let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+ let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
+ (sigma,ev,ev') in
+ let term = mkLetIn (Name id, ev, t, EConstr.Vars.subst_var id ev') in
+ (sigma, term)
+ end)
+ end
+
+let internal_cut ?(check=true) = internal_cut_gen ~check true
+let internal_cut_rev ?(check=true) = internal_cut_gen ~check false
+
let assert_before_then_gen b naming t tac =
let open Context.Rel.Declaration in
Proofview.Goal.enter begin fun gl ->
let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
Tacticals.New.tclTHENLAST
- (Proofview.V82.tactic
- (fun gl ->
- try Tacmach.internal_cut b id t gl
- with Evarutil.ClearDependencyError (id,err) ->
- error_replacing_dependency (pf_env gl) (project gl) id err))
+ (internal_cut b id t)
(tac id)
end
@@ -463,11 +529,7 @@ let assert_after_then_gen b naming t tac =
Proofview.Goal.enter begin fun gl ->
let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
Tacticals.New.tclTHENFIRST
- (Proofview.V82.tactic
- (fun gl ->
- try Tacmach.internal_cut_rev b id t gl
- with Evarutil.ClearDependencyError (id,err) ->
- error_replacing_dependency (pf_env gl) (project gl) id err))
+ (internal_cut_rev b id t)
(tac id)
end
@@ -999,29 +1061,10 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
in
aux n []
-let get_next_hyp_position id gl =
- let rec aux = function
- | [] -> raise (RefinerError (NoSuchHyp id))
- | decl :: right ->
- if Id.equal (NamedDecl.get_id decl) id then
- match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveLast
- else
- aux right
- in
- aux (Proofview.Goal.hyps (Proofview.Goal.assume gl))
-
-let get_previous_hyp_position id gl =
- let rec aux dest = function
- | [] -> raise (RefinerError (NoSuchHyp id))
- | decl :: right ->
- let hyp = NamedDecl.get_id decl in
- if Id.equal hyp id then dest else aux (MoveAfter hyp) right
- in
- aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
-
let intro_replacing id =
Proofview.Goal.enter begin fun gl ->
- let next_hyp = get_next_hyp_position id gl in
+ let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+ let next_hyp = get_next_hyp_position id hyps in
Tacticals.New.tclTHENLIST [
clear_for_replacing [id];
introduction id;
@@ -1040,7 +1083,8 @@ let intro_replacing id =
let intros_possibly_replacing ids =
let suboptimal = true in
Proofview.Goal.enter begin fun gl ->
- let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
+ let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+ let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in
Tacticals.New.tclTHEN
(Tacticals.New.tclMAP (fun id ->
Tacticals.New.tclTRY (clear_for_replacing [id]))
@@ -1053,7 +1097,8 @@ let intros_possibly_replacing ids =
(* This version assumes that replacement is actually possible *)
let intros_replacing ids =
Proofview.Goal.enter begin fun gl ->
- let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
+ let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+ let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in
Tacticals.New.tclTHEN
(clear_for_replacing ids)
(Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)
@@ -2578,7 +2623,8 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
Proofview.Goal.enter begin fun gl ->
let destopt =
if with_evars then MoveLast (* evars would depend on the whole context *)
- else get_previous_hyp_position id gl in
+ else
+ get_previous_hyp_position id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) in
let naming,ipat_tac =
prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in
let lemmas_target, last_lemma_target =
@@ -3074,17 +3120,17 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
*)
-let warn_unused_intro_pattern =
+let warn_unused_intro_pattern env sigma =
CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics"
(fun names ->
strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern")
++ str": " ++ prlist_with_sep spc
(Miscprint.pr_intro_pattern
- (fun c -> Printer.pr_econstr (snd (c (Global.env()) Evd.empty)))) names)
+ (fun c -> Printer.pr_econstr (snd (c env sigma)))) names)
-let check_unused_names names =
+let check_unused_names env sigma names =
if not (List.is_empty names) then
- warn_unused_intro_pattern names
+ warn_unused_intro_pattern env sigma names
let intropattern_of_name gl avoid = function
| Anonymous -> IntroNaming IntroAnonymous
@@ -3204,8 +3250,12 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
peel_tac ra' dests names thin)
end
| [] ->
- check_unused_names names;
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ check_unused_names env sigma names;
Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests)
+ end
in
peel_tac ra dests names []
@@ -3272,7 +3322,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
| Var id -> id
| _ ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
- id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in
+ id_of_name_using_hdchar env sigma (type_of c) Anonymous in
let x = fresh_id_in_env avoid id env in
Tacticals.New.tclTHEN
(letin_tac None (Name x) c None allHypsAndConcl)
@@ -3805,11 +3855,12 @@ let compare_upto_variables sigma x y =
in
compare x y
-let specialize_eqs id gl =
+let specialize_eqs id =
let open Context.Rel.Declaration in
- let env = Tacmach.pf_env gl in
- let ty = Tacmach.pf_get_hyp_typ gl id in
- let evars = ref (project gl) in
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let ty = Tacmach.New.pf_get_hyp_typ id gl in
+ let evars = ref (Proofview.Goal.sigma gl) in
let unif env evars c1 c2 =
compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2
in
@@ -3852,16 +3903,18 @@ let specialize_eqs id gl =
and acc' = Tacred.whd_simpl env !evars acc' in
let ty' = Evarutil.nf_evar !evars ty' in
if worked then
- tclTHENFIRST (Tacmach.internal_cut true id ty')
- (Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl
- else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
-
+ Tacticals.New.tclTHENFIRST
+ (internal_cut true id ty')
+ (exact_no_check ((* refresh_universes_strict *) acc'))
+ else
+ Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id)
+ end
let specialize_eqs id = Proofview.Goal.enter begin fun gl ->
let msg = str "Specialization not allowed on dependent hypotheses" in
Proofview.tclOR (clear [id])
(fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () ->
- Proofview.V82.tactic (specialize_eqs id)
+ specialize_eqs id
end
let occur_rel sigma n c =
@@ -4485,7 +4538,7 @@ let induction_gen clear_flag isrec with_evars elim
declaring the induction argument as a new local variable *)
let id =
(* Type not the right one if partially applied but anyway for internal use*)
- let x = id_of_name_using_hdchar (Global.env()) evd t Anonymous in
+ let x = id_of_name_using_hdchar env evd t Anonymous in
new_fresh_id [] x gl in
let info_arg = (is_arg_pure_hyp, not enough_applied) in
pose_induction_arg_then
@@ -4521,8 +4574,9 @@ let induction_gen_l isrec with_evars elim names lc =
Proofview.Goal.enter begin fun gl ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
let sigma = Tacmach.New.project gl in
+ Proofview.tclENV >>= fun env ->
let x =
- id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in
+ id_of_name_using_hdchar env sigma (type_of c) Anonymous in
let id = new_fresh_id [] x gl in
let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
@@ -4741,8 +4795,9 @@ let prove_symmetry hdcncl eq_kind =
one_constructor 1 NoBindings ])
let match_with_equation sigma c =
+ Proofview.tclENV >>= fun env ->
try
- let res = match_with_equation sigma c in
+ let res = match_with_equation env sigma c in
Proofview.tclUNIT res
with NoEquationFound ->
Proofview.tclZERO NoEquationFound
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 00:57:21 +0000