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, 9 insertions, 5 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 7b5690e2cc..439f462642 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -334,9 +334,13 @@ let map_fl f cfl = { cfl with rebus=f cfl.rebus }
     (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
 *)
 
-type instance_status =
-  | IsSuperType | IsSubType
-  | ConvUpToEta of int | Coercible of types | Processed
+type instance_constraint =
+    IsSuperType | IsSubType | ConvUpToEta of int | UserGiven
+
+type instance_typing_status =
+    TypeNotProcessed | TypeProcessed
+
+type instance_status = instance_constraint * instance_typing_status
 
 (* Clausal environments *)
 
@@ -543,7 +547,7 @@ let retract_coercible_metas evd =
   let mc,ml = 
     Metamap.fold (fun n v (mc,ml) -> 
       match v with
-	| Clval (na,(b,s),typ) when s <> Processed ->
+	| Clval (na,(b,(UserGiven,TypeNotProcessed as s)),typ) ->
 	    (n,b.rebus,s)::mc, Metamap.add n (Cltyp (na,typ)) ml
 	| v ->
 	    mc, Metamap.add n v ml)
@@ -556,7 +560,7 @@ let rec list_assoc_in_triple x = function
 
 let subst_defined_metas bl c = 
   let rec substrec c = match kind_of_term c with
-    | Meta i -> list_assoc_in_triple i bl
+    | Meta i -> substrec (list_assoc_in_triple i bl)
     | _ -> map_constr substrec c
   in try Some (substrec c) with Not_found -> None