From 9d2ebaa610b0fde6354cf86e4bbfae95cec71f09 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 28 May 2007 22:54:04 +0000 Subject: Contrôle de la compatibilité de apply via une information dans les métas permettant de savoir si une instance de méta vient d'un with-binding ou d'une unification, et si elle a déjà été typée ou pas. 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@9866 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/reductionops.ml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'pretyping/reductionops.ml') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7f05b1cbf..f247f47b6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -896,8 +896,8 @@ let meta_value evd mv = let meta_reducible_instance evd b = let fm = Metaset.elements b.freemetas in - let s = List.fold_left (fun l mv -> - try let g,s = meta_fvalue evd mv in (mv,(g.rebus,s))::l + let metas = List.fold_left (fun l mv -> + try let g,(_,s) = meta_fvalue evd mv in (mv,(g.rebus,s))::l with Anomaly _ | Not_found -> l) [] fm in let rec irec u = let u = whd_betaiota u in @@ -906,8 +906,8 @@ let meta_reducible_instance evd b = let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in (match try - let g,s = List.assoc m s in - if isConstruct g or s = Processed then Some g else None + let g,s = List.assoc m metas in + if isConstruct g or s = TypeProcessed then Some g else None with Not_found -> None with | Some g -> irec (mkCase (ci,p,g,bl)) @@ -916,15 +916,15 @@ let meta_reducible_instance evd b = let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in (match try - let g,s = List.assoc m s in - if isLambda g or s = Processed then Some g else None + let g,s = List.assoc m metas in + if isLambda g or s = TypeProcessed then Some g else None with Not_found -> None - with - | Some g -> irec (mkApp (g,l)) - | None -> mkApp (f,Array.map irec l)) + with + | Some g -> irec (mkApp (g,l)) + | None -> mkApp (f,Array.map irec l)) | Meta m -> - (try let g,s = List.assoc m s in if s = Processed then irec g else u - with Not_found -> u) + (try let g,s = List.assoc m metas in if s=TypeProcessed then irec g else u + with Not_found -> u) | _ -> map_constr irec u in if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus -- cgit v1.2.3