Prise en compte d'un type dont la sorte est une evar

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5710 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 1 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 52f899587a..49baf2ade5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -895,8 +895,17 @@ and pretype_type valcon env isevars lvar = function
       if !compter then nbimpl:=!nbimpl+1;
       (match valcon with
 	 | Some v ->
+             let s =
+               let sigma = evars_of isevars in
+               let t = Retyping.get_type_of env sigma v in
+               match kind_of_term (whd_betadeltaiota env sigma t) with
+                 | Sort s -> s
+                 | Evar v when is_Type (existential_type sigma v) -> 
+                     define_evar_as_sort isevars v
+                 | _ -> anomaly "Found a type constraint which is not a type"
+             in
 	     { utj_val = v;
-	       utj_type = Retyping.get_sort_of env (evars_of isevars) v }
+	       utj_type = s }
 	 | None ->
 	     let s = new_Type_sort () in
 	     { utj_val = new_isevar isevars env loc (mkSort s);