diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 10 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 4 |
5 files changed, 13 insertions, 10 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 853410db8..ef3845857 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -72,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c exception NotExtensibleClause let clenv_push_prod cl = - let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in + let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in let rec clrec typ = match kind_of_term typ with | Cast (t,_,_) -> clrec t | Prod (na,t,u) -> diff --git a/proofs/logic.ml b/proofs/logic.ml index fd8a70c65..bfaeae712 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -463,7 +463,7 @@ and mk_hdgoals sigma goal goalacc trm = and mk_arggoals sigma goal goalacc funty allargs = let foldmap (goalacc, funty, sigma) harg = - let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in + let t = whd_all (Goal.V82.env sigma goal) sigma funty in let rec collapse t = match kind_of_term t with | LetIn (_, c1, _, b) -> collapse (subst1 c1 b) | _ -> t diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index ee5591521..55dfb88b4 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -146,7 +146,10 @@ let make_flag_constant = function let make_flag env f = let red = no_red in let red = if f.rBeta then red_add red fBETA else red in - let red = if f.rIota then red_add red fIOTA else red in + let red = + if f.rIota then (red_add (red_add (red_add red fMATCH) fFIX) fCOFIX) + else red + in let red = if f.rZeta then red_add red fZETA else red in let red = if f.rDelta then (* All but rConst *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 8c0b4ba98..50984c48e 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -84,7 +84,7 @@ let pf_eapply f gls x = let pf_reduce = pf_apply let pf_e_reduce = pf_apply -let pf_whd_betadeltaiota = pf_reduce whd_betadeltaiota +let pf_whd_all = pf_reduce whd_all let pf_hnf_constr = pf_reduce hnf_constr let pf_nf = pf_reduce simpl let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) @@ -101,7 +101,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let pf_hnf_type_of gls = pf_whd_betadeltaiota gls % pf_get_type_of gls +let pf_hnf_type_of gls = pf_whd_all gls % pf_get_type_of gls let pf_is_matching = pf_apply Constr_matching.is_matching_conv let pf_matches = pf_apply Constr_matching.matches_conv @@ -219,7 +219,7 @@ module New = struct let sigma = project gl in nf_evar sigma concl - let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t + let pf_whd_all gl t = pf_apply whd_all gl t let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t @@ -228,11 +228,11 @@ module New = struct let pf_hnf_constr gl t = pf_apply hnf_constr gl t let pf_hnf_type_of gl t = - pf_whd_betadeltaiota gl (pf_get_type_of gl t) + pf_whd_all gl (pf_get_type_of gl t) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t + let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 182433cb3..100ed1522 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -63,7 +63,7 @@ val pf_e_reduce : (env -> evar_map -> constr -> evar_map * constr) -> goal sigma -> constr -> evar_map * constr -val pf_whd_betadeltaiota : goal sigma -> constr -> constr +val pf_whd_all : goal sigma -> constr -> constr val pf_hnf_constr : goal sigma -> constr -> constr val pf_nf : goal sigma -> constr -> constr val pf_nf_betaiota : goal sigma -> constr -> constr @@ -127,7 +127,7 @@ module New : sig val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types - val pf_whd_betadeltaiota : ('a, 'r) Proofview.Goal.t -> constr -> constr + val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map |