From 321acf47aa972fc6af9f62ccedf4af6e627497ec Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 8 Dec 2004 17:25:21 +0000 Subject: Bugs dans la déclaration du type du terme filtré si non défini MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6433 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/cases.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'pretyping') 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 -- cgit v1.2.3