Work on dep types pattern matching

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

4 files changed, 32 insertions, 2 deletions

diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index b11cc9d73d..4691afb157 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -158,6 +158,7 @@ module Coercion = struct
 		     let existS = Lazy.force existS in
 		     let prod = Lazy.force prod in
 		       if len = Array.length l' && len = 2 && i = i'
+			 && (i = Term.destInd existS.typ || i = Term.destInd prod.typ)
 		       then 
 			 if i = Term.destInd existS.typ 
 			 then
@@ -198,7 +199,7 @@ module Coercion = struct
 					  in
 					    mkApp (existS.intro, [| a'; pb'; x ; y |]))
 			   end
-			 else if i = Term.destInd prod.typ then
+			 else 
 			   begin 
 			     debug 1 (str "In coerce prod types");
 			     let (a, b), (a', b') = 
@@ -219,8 +220,22 @@ module Coercion = struct
 					  in
 					    mkApp (prod.intro, [| a'; b'; x ; y |]))
 			   end
+		       else
+			 if len = 1 && len = Array.length l' && i = i' then
+			   let argx, argy = l.(0), l'.(0) in
+			   let indtyp = Inductiveops.type_of_inductive env i in
+			   let argname, argtype, rest = destProd indtyp in
+			   let eq =
+			     mkApp (Lazy.force eqind, [| argtype; argx; argy |])
+			   in
+			   let pred = mkLambda (argname, argtype, 
+						mkApp (mkInd i, [| mkRel 1 |]))
+			   in
+			   let evar = make_existential dummy_loc env isevars eq in
+			     Some (fun x ->
+				     mkApp (Lazy.force eqrec, 
+					    [| argtype; argx; pred; x; argy; evar |]))
 			 else subco ()
-		       else subco ()
 		 | _ ->  subco ())
 	  | _, _ ->  subco ()
 
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 3279ad4c51..d476b4cd8d 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -46,6 +46,7 @@ let build_sig () =
 let sig_ = lazy (build_sig ())
 
 let eqind = lazy (init_constant ["Init"; "Logic"] "eq")
+let eqrec = lazy (init_constant ["Init"; "Logic"] "eq_rec")
 let eqind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
 let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
 
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 86662c478d..a0d9f6f56f 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -32,6 +32,7 @@ val proj2_sig_ref : reference
 val build_sig : unit -> coq_sigma_data
 val sig_ : coq_sigma_data lazy_t
 val eqind : constr lazy_t
+val eqrec : constr lazy_t
 val eqind_ref : global_reference lazy_t
 val refl_equal_ref : global_reference lazy_t
 val boolind : constr lazy_t
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 39fdc9ba75..55e5e90352 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -1,3 +1,16 @@
+Print eq_rec.
+Print eq.
+Inductive vector : nat -> Set :=
+  | vnil : vector 0
+  | vcons : nat -> forall n, vector n -> vector (S n).
+Set Printing All.
+Print eq.
+Program Fixpoint vapp (n m : nat) (v : vector n) (w : vector m) { struct v } : vector (n + m) :=
+  match v with
+  | vnil => w
+  | vcons a n' v' => vcons a (n' + m) (vapp n' m v' w)
+  end.
+
 
 Notation "( x & y )" := (@existS _ _ x y) : core_scope.
 Unset Printing All.