diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 14 | ||||
| -rw-r--r-- | proofs/refiner.ml | 2 |
2 files changed, 8 insertions, 8 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0a44eff874..5973e22e97 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -38,10 +38,10 @@ let new_evar_in_sign env = DOPN(Evar ev, Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps))) -let rec whd_deltat wc = function +let rec w_whd_evar wc = function | DOPN(Evar ev,_) as k -> if is_defined (w_Underlying wc) ev then - whd_deltat wc (w_const_value wc k) + w_whd_evar wc (w_const_value wc k) else collapse_appl k | t -> @@ -81,8 +81,8 @@ let mimick_evar hdc nargs sp wc = let unify_0 mc wc m n = let rec unirec_rec ((metasubst,evarsubst) as substn) m n = - let cM = whd_deltat wc m - and cN = whd_deltat wc n in + let cM = w_whd_evar wc m + and cN = w_whd_evar wc n in try match (cM,cN) with | DOP2(Cast,c,_),t2 -> unirec_rec substn c t2 @@ -166,7 +166,7 @@ let unify_0 mc wc m n = unirec_rec (mc,[]) m n -let whd_castappdeltat_stack sigma = +let whd_castappevar_stack sigma = let rec whrec x l = match x with | DOPN(Evar ev,_) as c -> @@ -180,9 +180,9 @@ let whd_castappdeltat_stack sigma = in whrec -let whd_castappdeltat sigma c = applist(whd_castappdeltat_stack sigma c []) +let whd_castappevar sigma c = applist(whd_castappevar_stack sigma c []) -let w_whd wc c = whd_castappdeltat (w_Underlying wc) c +let w_whd wc c = whd_castappevar (w_Underlying wc) c (* Unification * diff --git a/proofs/refiner.ml b/proofs/refiner.ml index c5e77abfba..3af8748035 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -684,7 +684,7 @@ let extract_pftreestate pts = 'sPC; 'sTR"Please ascend to the root" >]; let env = pts.tpf.goal.evar_env in let hyps = Environ.var_context env in - strong whd_betadeltatiota env (ts_it pts.tpfsigma) + strong whd_betaiotaevar env (ts_it pts.tpfsigma) (extract_proof hyps pts.tpf) |