From 86d3fe83df6a09dec54d70173698fd0cbe9a4e03 Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 5 Jun 2008 13:43:30 +0000
Subject: 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
---
 pretyping/unification.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 13587c9d75..ca1be55bb8 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)
 
-- 
cgit v1.2.3