correction de bug dans Function et augmentation de la classe des fonctions supportees

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

5 files changed, 301 insertions, 164 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index bd4cd0d8c9..be50c4bdbe 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -620,35 +620,41 @@ let build_proof
     : tactic =
   let rec build_proof_aux do_finalize dyn_infos : tactic = 
     fun g -> 
-      
 (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
 	match kind_of_term dyn_infos.info with 
-	  | Case(_,_,t,_) -> 
-	      let g_nb_prod = nb_prod (pf_concl g) in
-	      let type_of_term = pf_type_of g t in
-	      let term_eq =
-		make_refl_eq type_of_term t
+	  | Case(ci,ct,t,cb) -> 
+	      let do_finalize_t dyn_info' = 
+		fun g ->
+		  let t = dyn_info'.info in 
+		  let dyn_infos = {dyn_info' with info = 
+		      mkCase(ci,ct,t,cb)} in
+		  let g_nb_prod = nb_prod (pf_concl g) in
+		  let type_of_term = pf_type_of g t in
+		  let term_eq =
+		    make_refl_eq type_of_term t
+		  in
+		  tclTHENSEQ
+		    [
+		      h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+		      thin dyn_infos.rec_hyps;
+		      pattern_option [[-1],t] None;
+		      h_simplest_case t;
+		      (fun g' -> 
+			 let g'_nb_prod = nb_prod (pf_concl g') in 
+			 let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
+			 		     observe_tac "treat_new_case"
+			 (treat_new_case  
+			    ptes_infos
+			    nb_instanciate_partial 
+			    (build_proof do_finalize) 
+			    t 
+			    dyn_infos)
+			   g'
+		      )
+			
+		    ] g
 	      in
-	      tclTHENSEQ
-		[
-		  h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
-		  thin dyn_infos.rec_hyps;
-		  pattern_option [[-1],t] None;
-		  h_simplest_case t;
-		  (fun g' -> 
-		     let g'_nb_prod = nb_prod (pf_concl g') in 
-		     let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
-(* 		     observe_tac "treat_new_case"  *)
-		       (treat_new_case  
-		       ptes_infos
-		       nb_instanciate_partial 
-		       (build_proof do_finalize) 
-		       t 
-		       dyn_infos)
-		       g'
-		  )
-		  
-		] g
+	      build_proof do_finalize_t {dyn_infos with info = t} g
 	  | Lambda(n,t,b) ->
 	      begin
 		match kind_of_term( pf_concl g) with
@@ -752,7 +758,7 @@ let build_proof
 	  | Rel _ -> anomaly "Free var in goal conclusion !" 
   and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
-     (build_proof_aux do_finalize dyn_infos) g
+    observe_tac "build_proof" (build_proof_aux do_finalize dyn_infos) g
   and build_proof_args do_finalize dyn_infos (* f_args'  args *) :tactic =
     fun g ->
       let (f_args',args) = dyn_infos.info in 
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 04110ea989..9ec02d4c48 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -478,7 +478,72 @@ let generalize_depedent_of x hyp g =
 
 
 
-
+    (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis 
+       (unfolding, substituting, destructing cases \ldots)
+    *)
+let  rec intros_with_rewrite g = 
+  observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
+and intros_with_rewrite_aux : tactic = 
+  fun g -> 
+    let eq_ind = Coqlib.build_coq_eq () in 
+    match kind_of_term (pf_concl g) with 
+	  | Prod(_,t,t') -> 
+	      begin 
+		match kind_of_term t with 
+		  | App(eq,args) when (eq_constr eq eq_ind) -> 
+		      if isVar args.(1)
+		      then 			
+			let id = pf_get_new_id (id_of_string "y") g  in 
+			tclTHENSEQ [ h_intro id;
+				     generalize_depedent_of (destVar args.(1)) id; 
+				     tclTRY (Equality.rewriteLR (mkVar id));
+				     intros_with_rewrite
+				   ] 
+			  g
+		      else
+			begin 
+			  let id = pf_get_new_id (id_of_string "y") g  in 
+			  tclTHENSEQ[
+			    h_intro id;
+			    tclTRY (Equality.rewriteLR (mkVar id));
+			    intros_with_rewrite
+			  ] g
+			end
+		  | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> 
+		      Tauto.tauto g
+		  | Case(_,_,v,_) -> 
+		      tclTHENSEQ[
+			h_case (v,Rawterm.NoBindings);
+			intros_with_rewrite
+		      ] g
+		  | LetIn _ -> 
+		      tclTHENSEQ[
+			h_reduce 
+			  (Rawterm.Cbv
+			     {Rawterm.all_flags 
+			      with Rawterm.rDelta = false; 		 
+			     }) 
+			  onConcl
+			;
+			intros_with_rewrite
+		      ] g
+		  | _ -> 			
+		      let id = pf_get_new_id (id_of_string "y") g  in 
+		      tclTHENSEQ [ h_intro id;intros_with_rewrite] g
+	      end
+	  | LetIn _ -> 
+	      tclTHENSEQ[
+		h_reduce 
+		  (Rawterm.Cbv
+		     {Rawterm.all_flags 
+		      with Rawterm.rDelta = false; 		 
+		     }) 
+		  onConcl
+		;
+		intros_with_rewrite
+	      ] g
+	  | _ -> tclIDTAC g 
+  
 let rec reflexivity_with_destruct_cases g = 
   let destruct_case () = 
     try 
@@ -492,10 +557,34 @@ let rec reflexivity_with_destruct_cases g =
 	| _ -> reflexivity
     with _ -> reflexivity
   in
-  tclFIRST
+  let eq_ind =     Coqlib.build_coq_eq () in
+  let discr_inject =
+    Tacticals.onAllClauses (
+       fun sc g -> 
+	 match sc with 
+	     None -> tclIDTAC g
+	   | Some ((_,id),_) -> 
+	       match kind_of_term  (pf_type_of g (mkVar id)) with 
+		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> 
+		     if Equality.discriminable (pf_env g) (project g) t1 t2 
+		     then Equality.discr id g
+		     else if Equality.injectable (pf_env g) (project g) t1 t2
+		     then tclTHEN (Equality.inj [] id) intros_with_rewrite  g
+		     else tclIDTAC g
+		 | _ -> tclIDTAC g
+    )
+  in
+  (tclFIRST
     [ reflexivity;
-      destruct_case ()
-    ]
+      destruct_case ();
+      (*  We reach this point ONLY if 
+	  the same value is matched (at least) two times 
+	  along binding path.
+	  In this case, either we have a discriminable hypothesis and we are done, 
+	  either at least an injectable one and we do the injection before continuing
+      *)
+      tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases
+    ])
     g
 
 
@@ -566,7 +655,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	)
 	branches
     in
-    let eq_ind = Coqlib.build_coq_eq () in 
     (* We will need to change the function by its body 
        using [f_equation] if it is recursive (that is the graph is infinite 
        or unfold if the graph is finite 
@@ -596,71 +684,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	]
       else unfold_in_concl [([],Names.EvalConstRef (destConst f))]
     in
-    (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis 
-       (unfolding, substituting, destructing cases \ldots)
-    *)
-    let rec intros_with_rewrite_aux : tactic = 
-      fun g -> 
-	match kind_of_term (pf_concl g) with 
-	  | Prod(_,t,t') -> 
-	      begin 
-		match kind_of_term t with 
-		  | App(eq,args) when (eq_constr eq eq_ind) -> 
-		      if isVar args.(1)
-		      then 			
-			let id = pf_get_new_id (id_of_string "y") g  in 
-			tclTHENSEQ [ h_intro id;
-				     generalize_depedent_of (destVar args.(1)) id; 
-				     tclTRY (Equality.rewriteLR (mkVar id));
-				     intros_with_rewrite
-				   ] 
-			  g
-		      else
-			begin 
-			  let id = pf_get_new_id (id_of_string "y") g  in 
-			  tclTHENSEQ[
-			    h_intro id;
-			    tclTRY (Equality.rewriteLR (mkVar id));
-			    intros_with_rewrite
-			  ] g
-			end
-		  | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> 
-		      Tauto.tauto g
-		  | Case(_,_,v,_) -> 
-		      tclTHENSEQ[
-			h_case (v,Rawterm.NoBindings);
-			intros_with_rewrite
-		      ] g
-		  | LetIn _ -> 
-		      tclTHENSEQ[
-			h_reduce 
-			  (Rawterm.Cbv
-			     {Rawterm.all_flags 
-			      with Rawterm.rDelta = false; 		 
-			     }) 
-			  onConcl
-			;
-			intros_with_rewrite
-		      ] g
-		  | _ -> 			
-		      let id = pf_get_new_id (id_of_string "y") g  in 
-		      tclTHENSEQ [ h_intro id;intros_with_rewrite] g
-	      end
-	  | LetIn _ -> 
-	      tclTHENSEQ[
-		h_reduce 
-		  (Rawterm.Cbv
-		     {Rawterm.all_flags 
-		      with Rawterm.rDelta = false; 		 
-		     }) 
-		  onConcl
-		;
-		intros_with_rewrite
-	      ] g
-	  | _ -> tclIDTAC g 
-    and intros_with_rewrite g = 
-      observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
-    in
     (* The proof of each branche itself *)
     let ind_number = ref 0 in 
     let min_constr_number = ref 0 in
@@ -698,7 +721,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	h_intro graph_principle_id;
 	observe_tac "" (tclTHEN_i 
 	  (observe_tac "elim" ((elim (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings)))))
-	  (fun i g -> prove_branche i g ))
+	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
 
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 45f0a19752..7a2133a020 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -146,9 +146,8 @@ let rank_for_arg_list h =
   | x::tl -> if predicate h x then Some i else rank_aux (i+1) tl in
   rank_aux 0;;
 
-let rec (find_call_occs:
-	   constr -> constr -> (constr list ->constr)*(constr  list list)) =
- fun f expr ->
+let rec find_call_occs  =
+ fun nb_lam f expr ->
   match (kind_of_term expr) with
     App (g, args) when g = f -> 
       (fun l -> List.hd l), [Array.to_list args]
@@ -159,7 +158,7 @@ let rec (find_call_occs:
        | a::upper_tl ->
          (match find_aux upper_tl with
           (cf, ((arg1::args) as args_for_upper_tl)) -> 
-           (match find_call_occs f a with
+           (match find_call_occs nb_lam f a with
              cf2, (_ :: _ as other_args) ->
                let rec avoid_duplicates args =
                   match args with
@@ -183,7 +182,7 @@ let rec (find_call_occs:
                      other_args'@args_for_upper_tl
            | _, [] -> (fun x -> a::cf x), args_for_upper_tl)
 	 | _, [] ->
-	   (match find_call_occs f a with
+	   (match find_call_occs nb_lam f a with
 	     cf, (arg1::args) -> (fun l -> cf l::upper_tl), (arg1::args)
 	   | _, [] -> (fun x -> a::upper_tl), [])) in
      begin
@@ -192,22 +191,39 @@ let rec (find_call_occs:
 	 | cf, args ->
 	     (fun l -> mkApp (g, Array.of_list (cf l))), args
      end
-  | Rel(_) -> error "find_call_occs : Rel"
+  | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[])
   | Var(id) -> (fun l -> expr), []
   | Meta(_) -> error "find_call_occs : Meta"
   | Evar(_) -> error "find_call_occs : Evar"
   | Sort(_)  -> error "find_call_occs : Sort"
-  | Cast(b,_,_) -> find_call_occs f b
+  | Cast(b,_,_) -> find_call_occs nb_lam f b
   | Prod(_,_,_) -> error "find_call_occs : Prod"
-  | Lambda(_,_,_) -> error "find_call_occs : Lambda"
-  | LetIn(_,_,_,_) -> error "find_call_occs : let in"
+  | Lambda(na,t,b) -> 
+      begin
+	match find_call_occs (succ nb_lam) f b with 
+	  | _, [] ->  (* Lambda are authorized as long as they do not contain 
+			 recursives calls *)
+	      (fun l -> expr),[]
+	  | _ ->  error "find_call_occs : Lambda"
+      end
+  | LetIn(na,v,t,b) -> 
+      begin
+	match find_call_occs nb_lam f v, find_call_occs (succ nb_lam) f b with 
+	  | (_,[]),(_,[]) -> 
+	      ((fun l -> expr), [])
+	  | (_,[]),(cf,(_::_ as l)) -> 
+	      ((fun  l -> mkLetIn(na,v,t,cf l)),l)
+	  | (cf,(_::_ as l)),(_,[]) -> 
+	      ((fun l -> mkLetIn(na,cf l,t,b)), l)
+	  | _ -> error "find_call_occs : LetIn"
+      end
   | Const(_) -> (fun l -> expr), []
   | Ind(_) -> (fun l -> expr), []
   | Construct (_, _) -> (fun l -> expr), []
   | Case(i,t,a,r) ->
-      (match find_call_occs f a with
+      (match find_call_occs nb_lam f a with
 	cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args)
-      | _ -> (fun l -> mkCase(i, t, a, r)),[])
+      | _ -> (fun l -> expr),[])
   | Fix(_) -> error "find_call_occs : Fix"
   | CoFix(_) -> error "find_call_occs : CoFix";;
 
@@ -311,20 +327,8 @@ let  mkDestructEq not_on_hyp expr g =
 
 
 let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
-    cont_function (eqs:constr list) (expr:constr) g =
-  match kind_of_term expr with
-    | Lambda (n, _, b) -> 
-     	let n1 = 
-	  match n with
-      	      Name x -> x
-            | Anonymous -> ano_id
-	in
-     	let new_n = pf_get_new_id n1 g in
-	  tclTHEN (h_intro new_n)
-	    (mk_intros_and_continue thin_intros extra_eqn cont_function eqs 
-	       (subst1 (mkVar new_n) b)) g
-    | _ -> 
- 	if extra_eqn then
+    cont_function (eqs:constr list) nb_lam (expr:constr) g =
+  let finalize () =  	if extra_eqn then
 	  let teq = pf_get_new_id teq_id g in
 	    tclTHENLIST
 	      [ h_intro teq;
@@ -337,7 +341,7 @@ let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
 		(fun g1 -> 
 		   let ty_teq = pf_type_of g1 (mkVar teq) in 
 		   let teq_lhs,teq_rhs = 
-		     let _,args = destApp ty_teq in 
+		     let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal (sig_it g1) ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in 
 		     args.(1),args.(2) 
 		   in
 	           cont_function (mkVar teq::eqs) (replace_term teq_lhs teq_rhs expr) g1
@@ -350,7 +354,24 @@ let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
 	    h_intros thin_intros;
 	    cont_function eqs expr 
 	  ] g
-
+  in
+  if nb_lam = 0 
+  then finalize () 
+  else
+    match kind_of_term expr with
+      | Lambda (n, _, b) -> 
+     	  let n1 = 
+	    match n with
+      		Name x -> x
+              | Anonymous -> ano_id
+	  in
+     	  let new_n = pf_get_new_id n1 g in
+	  tclTHEN (h_intro new_n)
+	    (mk_intros_and_continue thin_intros extra_eqn cont_function eqs 
+	       (pred nb_lam) (subst1 (mkVar new_n) b)) g
+      | _ -> 
+	  assert false 
+(* 	  finalize () *)
 let const_of_ref = function
     ConstRef kn -> kn
   | _ -> anomaly "ConstRef expected"
@@ -599,10 +620,64 @@ let rec introduce_all_values is_mes acc_inv func context_fn
  
 	   
 let rec_leaf_terminate is_mes acc_inv hrec (func:global_reference) eqs expr =
-  match find_call_occs (mkVar (get_f (constr_of_reference func))) expr with
+  match find_call_occs 0 (mkVar (get_f (constr_of_reference func))) expr with
   | context_fn, args ->
       observe_tac "introduce_all_values" 
 	(introduce_all_values is_mes acc_inv func context_fn eqs  hrec args  [] [])
+(*
+let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier)  
+  (f_constr:constr) (func:global_reference) base_leaf rec_leaf = 
+  let rec proveterminate (eqs:constr list) (expr:constr)  =
+    try
+      (*  let _ = msgnl (str "entering proveterminate") in *)
+      let v =
+	match (kind_of_term expr) with
+	    Case (ci, t, a, l) -> 
+	      (match find_call_occs 0 f_constr a with
+		   _,[] ->
+		     (fun g -> 
+			let destruct_tac,rev_to_thin_intro = mkDestructEq rec_arg_id a g in 
+			tclTHENS destruct_tac
+			  (list_map_i 
+			     (fun i -> mk_intros_and_continue 
+				(List.rev rev_to_thin_intro) 
+				true 
+				proveterminate 
+				eqs
+				ci.ci_cstr_nargs.(i)
+			     )
+			     0
+			     (Array.to_list l) 
+			  ) g)
+		 | _, _::_ -> 
+		     (
+		       match find_call_occs  0 f_constr expr with
+	     		   _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr)
+			 | _, _:: _ -> 
+			     observe_tac "rec_leaf" 
+			       (rec_leaf is_mes acc_inv hrec  func eqs expr)
+		     )
+	      )
+	  | _ ->  (match find_call_occs  0 f_constr expr with
+	     	       _,[] -> 
+			 (try 
+			    observe_tac "base_leaf" (base_leaf func eqs expr)
+			  with e -> 
+			    (msgerrnl (str "failure in base case");raise e ))
+		     | _, _::_ -> 
+			 observe_tac "rec_leaf" 
+			   (rec_leaf is_mes acc_inv hrec  func eqs expr)
+		  ) in
+      (*  let _ = msgnl(str "exiting proveterminate") in *)
+      v
+    with e -> 
+      begin 
+	msgerrnl(str "failure in proveterminate"); 
+	raise e
+      end
+  in 
+  proveterminate 
+*)
 
 let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier)  
   (f_constr:constr) (func:global_reference) base_leaf rec_leaf = 
@@ -611,26 +686,33 @@ let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier)
       (*  let _ = msgnl (str "entering proveterminate") in *)
       let v =
 	match (kind_of_term expr) with
-	    Case (_, t, a, l) -> 
-	      (match find_call_occs f_constr a with
+	    Case (ci, t, a, l) -> 
+	      (match find_call_occs 0 f_constr a with
 		   _,[] ->
 		     (fun g -> 
 			let destruct_tac,rev_to_thin_intro = mkDestructEq rec_arg_id a g in 
 			tclTHENS destruct_tac
-			  (List.map 
-			     (mk_intros_and_continue (List.rev rev_to_thin_intro) true proveterminate eqs)
+			  (list_map_i 
+			     (fun i -> mk_intros_and_continue 
+				(List.rev rev_to_thin_intro) 
+				true 
+				proveterminate 
+				eqs
+				ci.ci_cstr_nargs.(i)
+			     )
+			     0
 			     (Array.to_list l) 
 			  ) g)
 		 | _, _::_ -> 
 		     (
-		       match find_call_occs  f_constr expr with
+		       match find_call_occs  0 f_constr expr with
 	     		   _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr)
 			 | _, _:: _ -> 
 			     observe_tac "rec_leaf" 
 			       (rec_leaf is_mes acc_inv hrec  func eqs expr)
 		     )
 	      )
-	  | _ ->  (match find_call_occs  f_constr expr with
+	  | _ ->  (match find_call_occs  0 f_constr expr with
 	     	       _,[] -> 
 			 (try 
 			    observe_tac "base_leaf" (base_leaf func eqs expr)
@@ -650,9 +732,9 @@ let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier)
   in 
   proveterminate 
 
-let hyp_terminates func = 
+let hyp_terminates nb_args func = 
   let a_arrow_b = arg_type (constr_of_reference func) in 
-  let rev_args,b = decompose_prod a_arrow_b in 
+  let rev_args,b = decompose_prod_n nb_args a_arrow_b in 
   let left = 
     mkApp(delayed_force iter, 
 	  Array.of_list 
@@ -776,7 +858,7 @@ let rec instantiate_lambda t l =
 ;;
 
 
-let whole_start is_mes func input_type relation rec_arg_num  : tactic = 
+let whole_start nb_args is_mes func input_type relation rec_arg_num  : tactic = 
   begin 
     fun g -> 
       let ids = ids_of_named_context (pf_hyps g) in
@@ -787,7 +869,7 @@ let whole_start is_mes func input_type relation rec_arg_num  : tactic =
 	  | Name f_id -> next_global_ident_away true f_id ids
 	  | Anonymous -> anomaly "Anonymous function"
       in
-      let n_names_types,_ = decompose_lam body1 in 
+      let n_names_types,_ = decompose_lam_n nb_args body1 in 
       let n_ids,ids = 
 	List.fold_left 
 	  (fun (n_ids,ids) (n_name,_) -> 
@@ -970,13 +1052,17 @@ let com_terminate
     input_type
     relation 
     rec_arg_num
-    thm_name using_lemmas hook =
+    thm_name using_lemmas 
+    nb_args
+    hook =
   let (evmap, env) = Command.get_current_context() in
   start_proof thm_name
     (Global, Proof Lemma) (Environ.named_context_val env)
-    (hyp_terminates fonctional_ref) hook;
-  by (observe_tac "whole_start" (whole_start is_mes fonctional_ref
-				       input_type relation rec_arg_num ));
+    (hyp_terminates nb_args fonctional_ref) hook;
+  by (observe_tac "whole_start" (whole_start nb_args is_mes fonctional_ref
+				   input_type relation rec_arg_num ))
+    
+  ;
   try 
     let new_goal_type = build_new_goal_type () in 
     open_new_goal using_lemmas tcc_lemma_ref
@@ -985,6 +1071,7 @@ let com_terminate
   with Failure "empty list of subgoals!" -> 
     (* a non recursive function declared with measure ! *)
     defined ()
+    
 
     
 
@@ -1156,12 +1243,12 @@ let rec introduce_all_values_eq  cont_tac functional termine
 			   let def_na,_,_ = destProd t in 
 			   Nameops.out_name k_na,Nameops.out_name def_na
 			 in
-			 observe_tac "general_rewrite_bindings" (general_rewrite_bindings false
+			 observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false
 			   (mkVar heq,
 			    ExplicitBindings
 			      [dummy_loc, NamedHyp k_id,
 			       f_S(mkVar pmax');
-			       dummy_loc, NamedHyp def_id, f]) false)
+			       dummy_loc, NamedHyp def_id, f]) false))
 			   g
 		     )
 		     [tclIDTAC;
@@ -1200,20 +1287,23 @@ let rec prove_eq  (termine:constr) (f:constr)(functional:global_reference)
   (expr:constr) =
 (*   tclTRY *)
   (match kind_of_term expr with
-      Case(_,t,a,l) ->
-	(match find_call_occs f a with
+      Case(ci,t,a,l) ->
+	(match find_call_occs 0 f a with
 	     _,[] -> 
 	       (fun g -> 
 		  let destruct_tac,rev_to_thin_intro = mkDestructEq [] a g in 
 		  tclTHENS destruct_tac
-		    (List.map 
-		       (mk_intros_and_continue (List.rev rev_to_thin_intro) true 
+		    (list_map_i  
+		       (fun i -> mk_intros_and_continue (List.rev rev_to_thin_intro) true 
 			  (prove_eq termine f functional)  
-			  eqs)
+			  eqs
+			  ci.ci_cstr_nargs.(i)
+		       )
+		       0
 		       (Array.to_list l) 
 		    ) g)
 	   | _,_::_ ->
-               	(match find_call_occs f expr with
+               	(match find_call_occs 0 f expr with
 	     _,[] -> base_leaf_eq functional eqs f
 	   | fn,args ->
 	       fun g ->
@@ -1222,7 +1312,7 @@ let rec prove_eq  (termine:constr) (f:constr)(functional:global_reference)
 		 (constr_of_reference functional)
 		 eqs expr fn args g))
        | _ -> 
-	   (match find_call_occs f expr with
+	   (match find_call_occs 0 f expr with
 		_,[] -> base_leaf_eq functional eqs f
 	      | fn,args ->
 		  fun g ->
@@ -1269,6 +1359,10 @@ let (com_eqn : identifier ->
     
     );;
 
+let nf_zeta env =       
+  Reductionops.clos_norm_flags  (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+    env
+    Evd.empty
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq 
     generate_induction_principle using_lemmas : unit =
@@ -1278,6 +1372,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in 
 (*   Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in 
+  let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in
+  let eq' = nf_zeta env_eq' eq'  in 
   let res = 
 (*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
 (*     Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
@@ -1308,28 +1404,32 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     let term_ref = Nametab.locate (make_short_qualid term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
 (*     message "start second proof"; *)
+    let stop = ref false in 
     begin 
       try com_eqn equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type)
       with e -> 
 	begin 
 	  if Tacinterp.get_debug () <> Tactic_debug.DebugOff
 	  then anomalylabstrm "" (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e);
-	  ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ());
-	  anomaly "Cannot create equation Lemma"
+	  stop := true;
+(* 	  ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *)
+(* 	  anomaly "Cannot create equation Lemma" *)
 	end
     end;
-    let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
-    let f_ref = destConst (constr_of_reference f_ref) 
-    and functional_ref = destConst (constr_of_reference functional_ref) 
-    and eq_ref = destConst (constr_of_reference eq_ref) in
-    generate_induction_principle f_ref tcc_lemma_constr
-     functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation;
-     if Options.is_verbose ()
-     then msgnl (h 1 (Ppconstr.pr_id function_name ++ 
-			spc () ++ str"is defined" )++ fnl () ++ 
-		   h 1 (Ppconstr.pr_id equation_id ++ 
-			  spc () ++ str"is defined" )
-		  )
+    if not !stop
+    then
+      let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
+      let f_ref = destConst (constr_of_reference f_ref) 
+      and functional_ref = destConst (constr_of_reference functional_ref) 
+      and eq_ref = destConst (constr_of_reference eq_ref) in
+      generate_induction_principle f_ref tcc_lemma_constr
+	functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation;
+      if Options.is_verbose ()
+      then msgnl (h 1 (Ppconstr.pr_id function_name ++ 
+			 spc () ++ str"is defined" )++ fnl () ++ 
+		    h 1 (Ppconstr.pr_id equation_id ++ 
+			   spc () ++ str"is defined" )
+		 )
   in
   try 
     com_terminate 
@@ -1340,7 +1440,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       relation rec_arg_num
       term_id
       using_lemmas
-      hook 
+      (List.length res_vars)
+      hook
   with e -> 
     begin
       ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ());
diff --git a/tactics/equality.ml b/tactics/equality.ml
index af5545fed2..d46b6f142a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -319,6 +319,12 @@ let discriminable env sigma t1 t2 =
     | Inl _ -> true
     | _ -> false
 
+let injectable env sigma t1 t2 = 
+    match find_positions env sigma t1 t2 with
+    | Inl _ | Inr [] -> false
+    | Inr _ -> true
+
+
 (* Once we have found a position, we need to project down to it.  If
    we are discriminating, then we need to produce False on one of the
    branches of the discriminator, and True on the other one.  So the
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 4aae8f8905..e7726eac32 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -107,6 +107,7 @@ val substHyp : bool -> types -> identifier -> tactic
 *)
 
 val discriminable : env -> evar_map -> constr -> constr -> bool
+val injectable : env -> evar_map -> constr -> constr -> bool
 
 (* Subst *)