From e0099553db47314521153393b1db2cb0bdc7fbe0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 Dec 2004 15:04:20 +0000
Subject: Relâchement obligation d'une contrainte de type sur les Hole en
 position terminale, pour plus grande généralité de understand_gen_tcc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6421 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0054c4770b..8389da9b3f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -274,10 +274,12 @@ let rec pretype tycon env isevars lvar = function
       anomaly "Found a pattern variable in a rawterm to type"
 	   
   | RHole (loc,k) ->
-      (match tycon with
-	 | Some ty ->
-	     { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
-	 | None -> error_unsolvable_implicit loc env (evars_of !isevars) k)
+      let ty =
+        match tycon with 
+          | Some ty -> ty
+          | None ->
+              e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
+      { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
 
   | RRec (loc,fixkind,names,bl,lar,vdef) ->
       let rec type_bl env ctxt = function
-- 
cgit v1.2.3