diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 04374c88b..ba0502ca4 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1167,7 +1167,8 @@ let local_whd_state_gen flags sigma = |_ -> s else s - | x -> s + | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _ | Ind _ | Proj _ -> s + in whrec @@ -1771,8 +1772,8 @@ let meta_reducible_instance evd b = let is_coerce = match s with CoerceToType -> true | _ -> false in if not is_coerce then irec g else u with Not_found -> u) - | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) -> - let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) in + | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) -> + let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in (match try let g, s = Metamap.find m metas in |