diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-05 13:43:30 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-05 13:43:30 +0000 |
| commit | 86d3fe83df6a09dec54d70173698fd0cbe9a4e03 (patch) | |
| tree | 8f6bdddca97c5b28dac0f80b18f08806495b2508 /pretyping | |
| parent | 49a0d1c36fee57db25c65ebfa71e46cf8b103eab (diff) | |
changed w_coerce_to_type to consider remaining unif problems (Hugo\'s patch)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11055 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 13587c9d7..ca1be55bb 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -411,8 +411,11 @@ let w_coerce_to_type env evd c cty mvty = let evd,mvty = pose_all_metas_as_evars env evd mvty in let tycon = mk_tycon_type mvty in let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in - let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in - (evd',j'.uj_val) + let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in + if b then + let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in + (evd',j'.uj_val) + else (evd,c) with e when precatchable_exception e -> (evd,c) |