diff options
author | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
commit | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch) | |
tree | 7b000ad50dcc45ff1c63768a983cded1e23a07ca /pretyping/unification.ml | |
parent | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff) |
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r-- | pretyping/unification.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index df5eff6a..fd045690 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -386,9 +386,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | Meta k, _ when not (dependent cM cN) (* helps early trying alternatives *) -> if wt && flags.check_applied_meta_types then - (let tyM = Typing.meta_type sigma k in - let tyN = get_type_of curenv sigma cN in - check_compatibility curenv substn tyM tyN); + (try + let tyM = Typing.meta_type sigma k in + let tyN = get_type_of curenv sigma cN in + check_compatibility curenv substn tyM tyN + with Anomaly _ (* Hack *) -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cN] does not contain any local variables *) if nb = 0 then sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst @@ -400,9 +403,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | _, Meta k when not (dependent cN cM) (* helps early trying alternatives *) -> if wt && flags.check_applied_meta_types then - (let tyM = get_type_of curenv sigma cM in - let tyN = Typing.meta_type sigma k in - check_compatibility curenv substn tyM tyN); + (try + let tyM = get_type_of curenv sigma cM in + let tyN = Typing.meta_type sigma k in + check_compatibility curenv substn tyM tyN + with Anomaly _ (* Hack *) -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cM] does not contain any local variables *) if nb = 0 then (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst) |