diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/contradiction.ml | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 9 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 2 | ||||
| -rw-r--r-- | tactics/leminv.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 20 |
6 files changed, 21 insertions, 20 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 316a79482f..63b5e2a702 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -533,7 +533,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = | Ind (i,_) -> is_class (IndRef i) | _ -> let env' = Environ.push_rel_context ctx env in - let ty' = whd_betadeltaiota env' ar in + let ty' = whd_all env' ar in if not (Term.eq_constr ty' ar) then iscl env' ty' else false in diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 26166bd834..c3796b4842 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -62,7 +62,7 @@ let contradiction_context = | d :: rest -> let id = get_id d in let typ = nf_evar sigma (get_type d) in - let typ = whd_betadeltaiota env sigma typ in + let typ = whd_all env sigma typ in if is_empty_type typ then simplest_elim (mkVar id) else match kind_of_term typ with @@ -84,7 +84,7 @@ let contradiction_context = end } let is_negation_of env sigma typ t = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Prod (na,t,u) -> let u = nf_evar sigma u in is_empty_type u && is_conv_leq env sigma typ t diff --git a/tactics/equality.ml b/tactics/equality.ml index 35be1fcb6e..24028b09df 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -400,7 +400,8 @@ let type_of_clause cls gl = match cls with let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> - let isatomic = isProd (whd_zeta hdcncl) in + let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let isatomic = isProd (whd_zeta evd hdcncl) in 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 c type_of_cls in @@ -720,8 +721,8 @@ let find_positions env sigma t1 t2 = then [(List.rev posn,t1,t2)] else [] in let rec findrec sorts posn t1 t2 = - let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in - let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in + let hd1,args1 = whd_all_stack env sigma t1 in + let hd2,args2 = whd_all_stack env sigma t2 in match (kind_of_term hd1, kind_of_term hd2) with | Construct (sp1,_), Construct (sp2,_) when Int.equal (List.length args1) (constructor_nallargs_env env sp1) @@ -1283,7 +1284,7 @@ let build_injector env sigma dflt c cpath = (* let try_delta_expand env sigma t = - let whdt = whd_betadeltaiota env sigma t in + let whdt = whd_all env sigma t in let rec hd_rec c = match kind_of_term c with | Construct _ -> whdt diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 4c2c84d23b..f2c72c2f3d 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -464,7 +464,7 @@ let match_eq_nf gls eqn (ref, hetero) = match Id.Map.bindings (pf_matches gls pat eqn) with | [(m1,t);(m2,x);(m3,y)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); - (t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y) + (t,pf_whd_all gls x,pf_whd_all gls y) | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms") let dest_nf_eq gls eqn = diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 70782ec648..63b1a7b541 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -114,7 +114,7 @@ let max_prefix_sign lid sign = | id::l -> snd (max_rec (id, sign_prefix id sign) l) *) let rec add_prods_sign env sigma t = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Prod (na,c1,b) -> let id = id_of_name_using_hdchar env t na in let b'= subst1 (mkVar id) b in @@ -167,7 +167,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in (pty,goal) in - let npty = nf_betadeltaiota env sigma pty in + let npty = nf_all env sigma pty in let extenv = push_named (LocalAssum (p,npty)) env in extenv, goal diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cf842d6f19..61aaef871d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -537,7 +537,7 @@ let fix ido n = match ido with mutual_fix id n [] 0 let rec check_is_mutcoind env sigma cl = - let b = whd_betadeltaiota env sigma cl in + let b = whd_all env sigma cl in match kind_of_term b with | Prod (na, c1, b) -> let open Context.Rel.Declaration in @@ -774,15 +774,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc = let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in if not b then if - isSort (whd_betadeltaiota env sigma t1) && - isSort (whd_betadeltaiota env sigma t2) + isSort (whd_all env sigma t1) && + isSort (whd_all env sigma t2) then (mayneedglobalcheck := true; sigma) else errorlabstrm "convert-check-hyp" (str "Types are incompatible.") else sigma end else - if not (isSort (whd_betadeltaiota env sigma t1)) then + if not (isSort (whd_all env sigma t1)) then errorlabstrm "convert-check-hyp" (str "Not a type.") else sigma @@ -1204,7 +1204,7 @@ let cut c = try (** Backward compat: ensure that [c] is well-typed. *) let typ = Typing.unsafe_type_of env sigma c in - let typ = whd_betadeltaiota env sigma typ in + let typ = whd_all env sigma typ in match kind_of_term typ with | Sort _ -> true | _ -> false @@ -2293,8 +2293,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in - let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in - let t = whd_betadeltaiota (type_of (mkVar id)) in + let whd_all = Tacmach.New.pf_apply whd_all gl in + let t = whd_all (type_of (mkVar id)) in let eqtac, thin = match match_with_equality_type t with | Some (hdcncl,[_;lhs;rhs]) -> if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then @@ -4253,7 +4253,7 @@ let check_enough_applied env sigma elim = | None -> (* No eliminator given *) fun u -> - let t,_ = decompose_app (whd_betadeltaiota env sigma u) in isInd t + let t,_ = decompose_app (whd_all env sigma u) in isInd t | Some elimc -> let elimt = Retyping.get_type_of env sigma (fst elimc) in let scheme = compute_elim_sig ~elimc elimt in @@ -4573,7 +4573,7 @@ let maybe_betadeltaiota_concl allowred gl = if not allowred then concl else let env = Proofview.Goal.env gl in - whd_betadeltaiota env sigma concl + whd_all env sigma concl let reflexivity_red allowred = Proofview.Goal.enter { enter = begin fun gl -> @@ -4944,7 +4944,7 @@ module New = struct let reduce_after_refine = reduce - (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) + (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]}) {onhyps=None; concl_occs=AllOccurrences } let refine ?unsafe c = |