Correction d'un vieux bug de coercion avec éta-expansion (utilisation

de subst1 au lieu de subst_term). Indentation plus compacte au passage.


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

2 files changed, 70 insertions, 54 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 30848ded11..0460b4177d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -177,59 +177,63 @@ module Default = struct
   let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
     try (the_conv_x_leq env t c1 isevars, v, t)
     with Reduction.NotConvertible ->
-      (try 
-	 inh_coerce_to_fail env isevars c1 v t
-	 with NoCoercion ->
-	   (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
-	      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
-		| Prod (_,t1,t2), Prod (name,u1,u2) -> 
-		    let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
-		    let (evd',b) =
-		      match v' with 
-			  Some v' ->
-			    (match kind_of_term v' with
-			       | Lambda (x,v1,v2) ->
-				   (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)  (* leq v1 u1? *)
-				    with Reduction.NotConvertible -> (isevars, None))
-			       | _  -> (isevars, None))
-			| None -> (isevars, None)
-		    in 
-		      (match b with
-			   Some (x, v1, v2) ->
-			     let env1 = push_rel (x,None,v1) env in
-			     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
-						       (Some v2) t2 u2 in
-			       (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', 
-				mkProd (x, v1, t2'))
-			 | None ->
-			     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
-			     (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
-			     (* has type (name:u1)u2 (with v' recursively obtained) *)
-			     let name = (match name with 
-					   | Anonymous -> Name (id_of_string "x")
-					   | _ -> name) in
-			     let env1 = push_rel (name,None,u1) env in
-			     let (evd', v1', t1') =
-			       inh_conv_coerce_to_fail loc env1 isevars
-				 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) 
-			     in
-			     let (evd'', v2', t2') = 
-			       let v2 =
-				 match v with 
-				     Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
-				   | None -> None
-			       and evd', t2 =
-				 match v1' with 
-				     Some v1' -> evd', subst1 v1' t2
-				   | None -> 
-				       let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in
-					 evd', subst1 ev t2
-			       in
-				 inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
-			     in
-			       (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
-				mkProd (name, u1, t2')))
-		| _ -> raise NoCoercion))
+    try inh_coerce_to_fail env isevars c1 v t
+    with NoCoercion ->
+    match
+      kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
+      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1)
+    with
+    | Prod (_,t1,t2), Prod (name,u1,u2) -> 
+	let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
+	let (evd',b) =
+	  match v' with 
+	  | Some v' ->
+	      (match kind_of_term v' with
+	       | Lambda (x,v1,v2) ->
+		   (* sous-typage non contravariant: pas de "leq v1 u1" *)
+		   (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)
+		   with Reduction.NotConvertible -> (isevars, None))
+	       | _  -> (isevars, None))
+	  | None -> (isevars, None)
+	in
+	(match b with
+	 | Some (x, v1, v2) ->
+	     let env1 = push_rel (x,None,v1) env in
+	     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
+	       (Some v2) t2 u2 in
+	     (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', 
+	     mkProd (x, v1, t2'))
+	 | None ->
+	     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
+	     (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
+	     (* has type (name:u1)u2 (with v' recursively obtained) *)
+	     let name = match name with 
+	       | Anonymous -> Name (id_of_string "x")
+	       | _ -> name
+	     in
+	     let env1 = push_rel (name,None,u1) env in
+	     let (evd', v1', t1') =
+	       inh_conv_coerce_to_fail loc env1 isevars
+		 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1)
+	     in
+	     let (evd'', v2', t2') = 
+	       let v2 =
+		 match v with 
+		 | Some v -> option_map (fun x -> mkApp(lift 1 v,[|x|])) v1'
+		 | None -> None
+	       and evd', t2 =
+		 match v1' with 
+		 | Some v1' -> evd', subst_term v1' t2
+		 | None -> 
+		     let evd', ev =
+		       new_evar evd' env ~src:(loc, InternalHole) t1' in
+		     evd', subst_term ev t2
+	       in
+	       inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
+	     in
+	     (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
+	     mkProd (name, u1, t2')))
+    | _ -> raise NoCoercion
 
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to loc env isevars cj (n, t) =
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index 8dd48752b1..750165a55a 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -22,7 +22,7 @@ Coercion i : h >-> nat.
 Parameter C : nat -> nat -> nat.
 Coercion C : nat >-> Funclass.
 
-(* Remark: in the following example, it cannot be decide whether C is
+(* Remark: in the following example, it cannot be decided whether C is
    from nat to Funclass or from A to nat. An explicit Coercion command is
    expected 
 
@@ -30,3 +30,15 @@ Parameter A : nat -> Prop.
 Parameter C:> forall n:nat, A n -> nat.
 *)
 
+(* Check coercion between products based on eta-expansion *)
+(* (there was a de Bruijn bug until rev ) *)
+
+Section P.
+
+Variable E : Set.
+Variables C D : E -> Prop.
+Variable G :> forall x, C x -> D x.
+
+Check fun (H : forall y:E, y = y -> C y) => (H : forall y:E, y = y -> D y).
+
+End P.