diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 5 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 1 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 7 |
4 files changed, 9 insertions, 6 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 43e0e9989..8a614d65f 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -202,8 +202,6 @@ let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) with Not_found -> None -let appterm_of_stack t = decompose_app (zip t) - let strong whdfun env sigma t = let rec strongrec env t = map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in @@ -551,7 +549,7 @@ let local_whd_state_gen flags sigma = let raw_whd_state_gen flags env sigma s = fst (whd_state_gen false flags env sigma s) let stack_red_of_state_red f sigma x = - appterm_of_stack (f sigma (x, empty_stack)) + decompose_app (zip (f sigma (x, empty_stack))) let red_of_state_red f sigma x = zip (f sigma (x,empty_stack)) @@ -560,6 +558,7 @@ let red_of_state_red f sigma x = let whd_nored_state = local_whd_state_gen nored let whd_nored_stack = stack_red_of_state_red whd_nored_state +let whd_nored = red_of_state_red whd_nored_state (* 1. Beta Reduction Functions *) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b98a7d309..664039206 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -115,6 +115,7 @@ val nf_betaiota_preserving_vm_cast : reduction_function (** Lazy strategy, weak head reduction *) val whd_evar : evar_map -> constr -> constr +val whd_nored : local_reduction_function val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betaiotazeta : local_reduction_function diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b8dbefb88..e49f88128 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1109,7 +1109,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = else (* lazily reduces to match the head of [t] with the expected [ref] *) let rec elimrec env t l = - let c, _ = Reductionops.whd_nored_stack sigma t in + let c, _ = decompose_appvect (Reductionops.whd_nored sigma t) in match kind_of_term c with | Prod (n,ty,t') -> if allow_product then diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 9c3b5c4df..ce18804d9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -969,13 +969,16 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd = [clenv_typed_unify M N clenv] expects in addition that expected types of metavars are unifiable with the types of their instances *) +let head_app sigma m = + fst (decompose_appvect (whd_nored sigma m)) + let check_types env flags (sigma,_,_ as subst) m n = - if isEvar_or_Meta (fst (whd_nored_stack sigma m)) then + if isEvar_or_Meta (head_app sigma m) then unify_0_with_initial_metas subst true env CUMUL flags (get_type_of env sigma n) (get_type_of env sigma m) - else if isEvar_or_Meta (fst (whd_nored_stack sigma n)) then + else if isEvar_or_Meta (head_app sigma n) then unify_0_with_initial_metas subst true env CUMUL flags (get_type_of env sigma m) |