Various little subtac fixes, add some useful tactics.

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

9 files changed, 46 insertions, 93 deletions

diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
index dae389ce30..17ebb44117 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/contrib/subtac/SubtacTactics.v
@@ -64,3 +64,12 @@ Ltac myinjection :=
           | _ => idtac
         end.
 
+Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0.
+
+Ltac bang :=
+  match goal with
+    | |- ?x => 
+      match x with
+        | context [False_rect _ ?p] => elim p
+      end
+  end.
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 102fa94ad4..686a5fd415 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -43,6 +43,13 @@ induction t.
  simpl ; auto.
 Qed.
 
+Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
+  f = g -> forall x, f x = g x.
+Proof.
+  intros.
+  rewrite H.
+  auto.
+Qed.
 
 Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; 
   try (solve [ red ; intros ; discriminate ]) ; auto with arith.  
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 17110c058c..088dc775b6 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -2026,7 +2026,6 @@ let liftn_rel_context n k sign =
 
 
 let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
-  let tycon0 = tycon in
   (* We build the matrix of patterns and right-hand-side *)
   let matx = matx_of_eqns env eqns in
      
@@ -2097,7 +2096,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
 	let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in
 	let j = 
 	  { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
-	    uj_type = out_some (valcon_of_tycon tycon0); }
+	    uj_type = lift (-tomatchs_len) (nf_isevar !isevars tycon_constr); }
 	in j
 (* 	  inh_conv_coerce_to_tycon loc env isevars j tycon0 *)
     else
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index f49fada5b9..41a3bdf233 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -120,13 +120,14 @@ module Coercion = struct
 (*       (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++  *)
 (* 		  str " to "++ my_print_constr env y) *)
 (*        with _ -> ()); *)
-      try 
-	isevars := the_conv_x_leq env x y !isevars;
-(* 	(try debug 1 (str "Unified " ++ (my_print_constr env x) ++  *)
-(* 			str " and "++ my_print_constr env y); *)
-(* 	 with _ -> ()); *)
-	None
-      with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
+      let x = hnf env isevars x and y = hnf env isevars y in
+	try 
+	  isevars := the_conv_x_leq env x y !isevars;
+	  (* 	(try debug 1 (str "Unified " ++ (my_print_constr env x) ++  *)
+	  (* 			str " and "++ my_print_constr env y); *)
+	  (* 	 with _ -> ()); *)
+	  None
+	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' =
@@ -245,14 +246,24 @@ module Coercion = struct
 			   end
 		       else
 			 if i = i' && len = Array.length l' then
-			   Some (coerce_application (Typing.type_of env (evars_of !isevars) c) c c' l l')
+			   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 () *)
 			 else
 			   subco ()
 		 | x, y when x = y ->
-		     let lam_type = Typing.type_of env (evars_of !isevars) c in
-		       if Array.length l = Array.length l' then (
-			 Some (coerce_application lam_type c c' l l')
-		       ) else subco ()
+		     if Array.length l = Array.length l' then
+		       let evm = evars_of !isevars 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')
+			 ) else subco ()
+		     else subco ()
 		 | _ -> subco ())
 	  | _, _ ->  subco ()
 
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index cab8829dbd..1220c13f4d 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -56,7 +56,6 @@ let interp_gen kind isevars env
                ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in
-  let c' = Subtac_utils.rewrite_cases env c' in
 (*     (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *)
   let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
     evar_nf isevars c'
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 7ae8f45d7a..2b36bd2d26 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -123,7 +123,6 @@ let subtac_process env isevars id l c tycon =
 	    mk_tycon coqt
   in    
   let c = coqintern !isevars env_binders c in
-  let c = Subtac_utils.rewrite_cases env c in
   let coqc, ctyp = interp env_binders isevars c tycon in
 (*   let _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++ *)
 (* 		 str "Coq type: " ++ my_print_constr env_binders ctyp) *)
@@ -137,11 +136,11 @@ let subtac_process env isevars id l c tycon =
   let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in
   let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp in
 
-(*   let _ = try trace (str "After evar normalization: " ++ spc () ++ *)
-(* 		 str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () *)
-(* 		 ++ str "Coq type: " ++ my_print_constr env fullctyp)  *)
-(*      with _ -> ()  *)
-(*   in *)
+  let _ = try trace (str "After evar normalization: " ++ spc () ++
+		 str "Coq term: " ++ my_print_constr env fullcoqc ++ spc ()
+		 ++ str "Coq type: " ++ my_print_constr env fullctyp)
+     with _ -> ()
+  in
   let evm = non_instanciated_map env isevars in
 (*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
     evm, fullcoqc, fullctyp
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index dc199c1d02..e53dad2659 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -93,7 +93,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
   (* coerce to tycon if any *)
   let inh_conv_coerce_to_tycon loc env isevars j = function
-    | None -> j
+    | None -> j_nf_isevar !isevars j
     | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t
 
   let push_rels vars env = List.fold_right push_rel vars env
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index e7e1dbcc52..51bb1f4bea 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -518,76 +518,6 @@ let list_mapi f =
     | [] -> []
   in aux 0
 
-open Rawterm
-
-let rewrite_cases_aux (loc, po, tml, eqns) =
-  let tml' = list_mapi (fun i (c, (n, opt)) -> c, 
-		       ((match n with
-			    Name id -> (match c with
-					  | RVar (_, id') when id = id' ->
-					      id, (id_of_string (string_of_id id ^ "Heq_id"))
-					  | RVar (_, id') ->
-					      id', id
-					  | _ -> id_of_string (string_of_id id ^ "Heq_id"), id)
-			   | Anonymous -> 
-			       let str = "Heq_id" ^ string_of_int i in
-				 id_of_string str, id_of_string (str ^ "'")),
-			opt)) tml 
-  in
-  let mkHole = RHole (dummy_loc, InternalHole) in
-  let mkCoerceCast c = RCast (dummy_loc, c, CastCoerce, mkHole) in
-  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eq_ind_ref)),
-		       [mkHole; c; n])
-  in
-  let eqs_types = 
-    List.map
-      (fun (c, ((id, id'), _)) ->
-	 let heqid = id_of_string ("Heq" ^ string_of_id id) in
-	   Name heqid, mkeq (RVar (dummy_loc, id')) c)
-      tml'
-  in
-  let po = 
-    List.fold_right
-      (fun (n,t) acc ->
-	 RProd (dummy_loc, Anonymous, t, acc))
-      eqs_types (match po with 
-		     Some e -> e
-		   | None -> mkHole)
-  in
-  let eqns =   
-    List.map (fun (loc, idl, cpl, c) ->
-		let c' = 
-		  List.fold_left 
-		    (fun acc (n, t) ->
-		       RLambda (dummy_loc, n, mkHole, acc))
-		    c eqs_types
-		in (loc, idl, cpl, c'))
-      eqns
-  in
-  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
-			      [mkHole; c])
-  in
-  let refls = List.map (fun (c, ((id, _), _)) -> mk_refl_equal (mkCoerceCast c)) tml' in
-  let tml'' = List.map (fun (c, ((id, id'), opt)) -> c, (Name id', opt)) tml' in
-  let case = RCases (loc,Some po,tml'',eqns) in
-  let app = RApp (dummy_loc, case, refls) in
-(*   let letapp = List.fold_left (fun acc (c, ((id, id'), opt)) -> RLetIn (dummy_loc, Name id, c, acc)) *)
-(* 		 app tml' *)
-(*   in *)
-    app
-
-let rec rewrite_cases c = 
-  match c with 
-      RCases _ -> let c' = map_rawconstr rewrite_cases c in
-	(match c' with 
-	   | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
-	   | _ -> assert(false))
-    | _ -> map_rawconstr rewrite_cases c
-	  
-let rewrite_cases env c = c
-(*   let c' = rewrite_cases c in *)
-(*   let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in *)
-(*     c' *)
 
 let id_of_name = function
     Name n -> n
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 756460b327..d042eab795 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -105,7 +105,6 @@ val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
 
 val destruct_ex : constr -> constr -> constr list
 
-val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
 val id_of_name : name -> identifier
 
 val definition_message : identifier -> unit