diff options
Diffstat (limited to 'pretyping')
| -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 f3014424c4..219c1ec227 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -382,9 +382,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 ~lax:true sigma cN in + check_compatibility curenv substn tyM tyN + with RetypeError _ -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cN] does not contain any local variables *) if Int.equal nb 0 then sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst @@ -396,9 +399,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 RetypeError _ -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cM] does not contain any local variables *) if Int.equal nb 0 then (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst) |