Bugs dans la déclaration du type du terme filtré si non défini

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

1 files changed, 5 insertions, 6 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9feb53531..9d336fc24 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -409,13 +409,12 @@ let inh_coerce_to_ind isevars env tmloc ty tyi =
   let hole_source = match tmloc with 
     | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (tyi,i))
     | None -> fun _ -> (dummy_loc, Evd.InternalHole) in
-   let (_,evarl,_) =
+   let (evarl,_) =
     List.fold_right
-      (fun (na,ty) (env,evl,n) ->
-	 (push_rel (na,None,ty) env,
-	    (e_new_evar isevars env ~src:(hole_source n) ty)::evl,n+1))
-      ntys (env,[],1) in
-  let expected_typ = applist (mkInd tyi,evarl) in
+      (fun (na,ty) (evl,n) ->
+	(e_new_evar isevars env ~src:(hole_source n) (substl evl ty))::evl,n+1)
+      ntys ([],1) in
+  let expected_typ = applist (mkInd tyi,List.rev evarl) in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
         un inductif cela doit être égal *)
   if e_cumul env isevars expected_typ ty then ty