diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /pretyping/reductionops.ml | |
parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'pretyping/reductionops.ml')
-rw-r--r-- | pretyping/reductionops.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index fddc7fc7..993ad46b 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -924,7 +924,10 @@ let meta_reducible_instance evd b = let u = whd_betaiota Evd.empty u in match kind_of_term u with | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) -> - let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in + let m = + try destMeta c + with e when Errors.noncritical e -> destMeta (pi1 (destCast c)) + in (match try let g,s = List.assoc m metas in @@ -934,7 +937,10 @@ let meta_reducible_instance evd b = | Some g -> irec (mkCase (ci,p,g,bl)) | None -> mkCase (ci,irec p,c,Array.map irec bl)) | App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) -> - let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in + let m = + try destMeta f + with e when Errors.noncritical e -> destMeta (pi1 (destCast f)) + in (match try let g,s = List.assoc m metas in |