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.


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

1 files changed, 11 insertions, 11 deletions

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