diff options
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) |