Fix myinjection tactic, generalize coercion for applications

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

2 files changed, 26 insertions, 11 deletions

diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index fc002a01be..08fa8fbc22 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -76,7 +76,10 @@ Ltac myinjection :=
           | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H
           | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H
           | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H
-          | [ H : ?f ?a ?b ?c ?d ?e ?f= ?f' ?a' ?b' ?c' ?d' ?e' ?f'  |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g'  |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H
           | _ => idtac
         end.
 
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 38a95e9bc0..8c95610f2e 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -86,6 +86,13 @@ module Coercion = struct
 
   let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c
 
+  let lift_args n sign =
+    let rec liftrec k = function
+      | t::sign -> liftn n k t :: (liftrec (k-1) sign)
+      | [] -> []
+    in
+      liftrec (List.length sign) sign
+
   let rec mu env isevars t =   
     let isevars = ref isevars in
     let rec aux v = 
@@ -123,20 +130,25 @@ module Coercion = struct
     and coerce' env x y : (Term.constr -> Term.constr) option =
       let subco () = subset_coerce env isevars x y in
       let rec coerce_application typ c c' l l' =
-	let rec aux typ i co = 
+	let rec aux tele typ i co = 
 	  trace (str"Inserting coercion at application");
 	  if i < Array.length l then
 	    let hdx = l.(i) and hdy = l'.(i) in
-	    let (n, eqT, restT) = destProd typ in
-	    let pred = mkLambda (n, eqT, mkApp (lift 1 c, [| mkRel 1 |])) in
-	    let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
-	    let evar = make_existential dummy_loc env isevars eq in
-	    let eq_app x = mkApp (Lazy.force eq_rect,
-				  [| eqT; hdx; pred; x; hdy; evar|])
-	    in 
-	      aux (subst1 hdy restT) (succ i) (fun x -> eq_app (co x))
+	      try isevars := the_conv_x_leq env hdx hdy !isevars;
+		let (n, eqT, restT) = destProd typ in
+		aux (hdx :: tele) (subst1 hdy restT) (succ i) co
+	      with Reduction.NotConvertible ->
+		let (n, eqT, restT) = destProd typ in
+		let args = List.rev (mkRel 1 :: lift_args 1 tele) in
+		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
+		let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
+		let evar = make_existential dummy_loc env isevars eq in
+		let eq_app x = mkApp (Lazy.force eq_rect,
+				      [| eqT; hdx; pred; x; hdy; evar|])
+		in 
+		  aux (hdx :: tele) (subst1 hdy restT) (succ i)  (fun x -> eq_app (co x))
 	  else co
-	in aux typ 0 (fun x -> x)
+	in aux [] typ 0 (fun x -> x)
       in
 (* 	(try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++  *)
 (* 		    str " to "++ my_print_constr env y); *)