diff options
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | kernel/term.ml | 5 | ||||
| -rw-r--r-- | kernel/term.mli | 3 | ||||
| -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 | ||||
| -rw-r--r-- | proofs/clenv.ml | 4 |
8 files changed, 20 insertions, 9 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 5fa6346f0..737687adc 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -558,7 +558,7 @@ let scope_class_compare sc1 sc2 = match sc1, sc2 with let scope_class_of_reference x = ScopeRef x let compute_scope_class t = - let t', _ = Reductionops.whd_betaiotazeta_stack Evd.empty t in + let t', _ = decompose_appvect (Reductionops.whd_betaiotazeta Evd.empty t) in match kind_of_term t' with | Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t') | Sort _ -> ScopeSort diff --git a/kernel/term.ml b/kernel/term.ml index fa204b570..44a10aa35 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -339,6 +339,11 @@ let decompose_app c = | App (f,cl) -> (f, Array.to_list cl) | _ -> (c,[]) +let decompose_appvect c = + match kind_of_term c with + | App (f,cl) -> (f, cl) + | _ -> (c,[||]) + (****************************************************************************) (* Functions for dealing with constr terms *) (****************************************************************************) diff --git a/kernel/term.mli b/kernel/term.mli index a3745d5e3..8131753fe 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -152,6 +152,9 @@ val destApplication : constr -> constr * constr array (** Decompose any term as an applicative term; the list of args can be empty *) val decompose_app : constr -> constr * constr list +(** Same as [decompose_app], but returns an array. *) +val decompose_appvect : constr -> constr * constr array + (** Destructs a constant *) val destConst : constr -> constant 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) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0df882b2b..a8bbfe127 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -255,7 +255,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags) clenv = let clenv_unique_resolver ?(flags=default_unify_flags) clenv gl = let concl = Goal.V82.concl clenv.evd (sig_it gl) in - if isMeta (fst (whd_nored_stack clenv.evd clenv.templtyp.rebus)) then + if isMeta (fst (decompose_appvect (whd_nored clenv.evd clenv.templtyp.rebus))) then clenv_unify CUMUL ~flags (clenv_type clenv) concl (clenv_unify_meta_types ~flags clenv) else @@ -408,7 +408,7 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta (fst (whd_nored_stack clenv.evd u)) then + if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else |