diff options
| -rw-r--r-- | pretyping/reductionops.ml | 12 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 3 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 8 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 |
4 files changed, 12 insertions, 13 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index b2a9bdcc5..e86732658 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -939,16 +939,10 @@ let splay_lam_n env sigma n = in decrec env n empty_rel_context -exception NotASort - -let decomp_sort env sigma t = +let is_sort env sigma t = match kind_of_term (whd_betadeltaiota env sigma t) with - | Sort s -> s - | _ -> raise NotASort - -let is_sort env sigma arity = - try let _ = decomp_sort env sigma arity in true - with NotASort -> false + | Sort s -> true + | _ -> false (* reduction to head-normal-form allowing delta/zeta only in argument of case/fix (heuristic used by evar_conv) *) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index e95fc41c0..588914c58 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -181,8 +181,6 @@ val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_prod_assum : env -> evar_map -> constr -> rel_context * constr -val decomp_sort : env -> evar_map -> types -> sorts -val is_sort : env -> evar_map -> types -> bool type 'a miota_args = { mP : constr; (** the result type *) @@ -196,6 +194,7 @@ val reduce_mind_case : constr miota_args -> constr val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term val is_arity : env -> evar_map -> constr -> bool +val is_sort : env -> evar_map -> types -> bool val whd_programs : reduction_function diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index c61872091..f5f977615 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -76,6 +76,11 @@ let sort_of_atomic_type env sigma ft args = | _ -> retype_error NotASort in concl_of_arity env ft (Array.to_list args) +let decomp_sort env sigma t = + match kind_of_term (whd_betadeltaiota env sigma t) with + | Sort s -> s + | _ -> retype_error NotASort + let type_of_var env id = try let (_,_,ty) = lookup_named id env in ty with Not_found -> retype_error (BadVariable id) @@ -165,7 +170,8 @@ let retype ?(polyprop=true) sigma = | App(f,args) -> family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> retype_error NotAType - | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) + | _ -> + family_of_sort (decomp_sort env sigma (type_of env t)) and type_of_global_reference_knowing_parameters env c args = let argtyps = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5dd794243..14d6ad333 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -950,7 +950,7 @@ let w_merge env with_types flags (evd,metas,evars) = else Evd.define sp (Evarutil.nf_evar evd''' c) evd''' in (* merge constraints *) - w_merge_rec evd (order_metas metas) evars [] + w_merge_rec evd (order_metas metas) (List.rev evars) [] let w_unify_meta_types env ?(flags=default_unify_flags) evd = let metas,evd = retract_coercible_metas evd in |