Various fixes:

- Fix a typo in lowercase_utf8
- Fix generation of signatures in subtac_cases not working for dependent
inductive types with dependent indices.
- Fix coercion of inductive types generating ill-typed terms.
- Fix test script using new syntax for Instances.
- Move simpl_existTs to Program.Equality and use it in simpl_depind.


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

2 files changed, 21 insertions, 14 deletions

diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 6a470afc6..45f0f0129 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1977,7 +1977,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 			     (lift (nargeqs + nar) arg),
 			   mk_eq_refl argt arg)
 			else
-			  (mk_JMeq (lift (nargeqs + slift) appt)
+			  (mk_JMeq (lift (nargeqs + slift) t)
 			     (mkRel (nargeqs + slift))
 			     (lift (nargeqs + nar) argt)
 			     (lift (nargeqs + nar) arg),
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 5ca313d0b..4a1869053 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -129,9 +129,9 @@ module Coercion = struct
 	with Reduction.NotConvertible -> coerce' env x y
     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 coerce_application typ typ' c c' l l' =
 	let len = Array.length l in
-	let rec aux tele typ i co = 
+	let rec aux tele typ typ' i co = 
 (* 	  (try trace (str "coerce_application.aux from " ++ (my_print_constr env x) ++ *)
 (* 			 str " to "++ my_print_constr env y *)
 (* 		       ++ str "in env:" ++ my_print_env env); *)
@@ -140,9 +140,15 @@ module Coercion = struct
 	    let hdx = l.(i) and hdy = l'.(i) in
 	      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
+		let (n', eqT', restT') = destProd typ' in
+		aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
 	      with Reduction.NotConvertible ->
 		let (n, eqT, restT) = destProd typ in
+		let (n', eqT', restT') = destProd typ' in
+		let _ = 
+		  try isevars := the_conv_x_leq env eqT eqT' !isevars
+		  with Reduction.NotConvertible -> raise NoSubtacCoercion
+		in
 		let restargs = lift_args 1 
 		  (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
 		in 
@@ -154,9 +160,9 @@ module Coercion = struct
 		let eq_app x = mkApp (Lazy.force eq_rect,
 				      [| eqT; hdx; pred; x; hdy; evar|]) in
 (* 		  trace (str"Inserting coercion at application"); *)
-		  aux (hdy :: tele) (subst1 hdy restT) (succ i)  (fun x -> eq_app (co x))
-	  else co
-	in aux [] typ 0 (fun x -> x)
+		  aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
+	  else Some co
+	in aux [] typ typ' 0 (fun x -> x)
       in
 (* 	(try trace (str "coerce' from " ++ (my_print_constr env x) ++ *)
 (* 		       str " to "++ my_print_constr env y *)
@@ -264,21 +270,22 @@ module Coercion = struct
 		       else
 			 if i = i' && len = Array.length l' then
 			   let evm = evars_of !isevars in
-			   let typ = Typing.type_of env evm c in
 			     (try subco () 
-			      with NoSubtacCoercion ->
-				
-(* 			     if not (is_arity env evm typ) then *)
-			       Some (coerce_application typ c c' l l'))
-(* 			     else subco () *)
+			       with NoSubtacCoercion ->
+				 let typ = Typing.type_of env evm c in
+				 let typ' = Typing.type_of env evm c' in
+				   (* 			     if not (is_arity env evm typ) then *)
+				   coerce_application typ typ' c c' l l')
+			       (* 			     else subco () *)
 			 else
 			   subco ()
 		 | x, y when x = y ->
 		     if Array.length l = Array.length l' then
 		       let evm = evars_of !isevars in
 		       let lam_type = Typing.type_of env evm c in
+		       let lam_type' = Typing.type_of env evm c' in
 (* 			 if not (is_arity env evm lam_type) then ( *)
-			   Some (coerce_application lam_type c c' l l')
+			 coerce_application lam_type lam_type' c c' l l'
 (* 			 ) else subco () *)
 		     else subco ()
 		 | _ -> subco ())