Ajout de eelim, ecase, edestruct et einduction (expérimental).

Ajout de l'option with à (e)destruct et (e)induction.



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

3 files changed, 7 insertions, 7 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 45dee78311..c68304c755 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -910,7 +910,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 	   let rec_id = pf_nth_hyp_id g 1 in
 	   tclTHENSEQ
 	     [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
-	      (* observe_tac "h_case" *) (h_case(mkVar rec_id,Rawterm.NoBindings));
+	      (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Rawterm.NoBindings));
 	      intros_reflexivity] g
 	)
       ]
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 0fa73f0963..199e01525b 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -22,8 +22,8 @@ let is_rec_info scheme_info =
 
 let choose_dest_or_ind scheme_info =
     if is_rec_info scheme_info
-    then Tactics.new_induct
-    else Tactics.new_destruct
+    then Tactics.new_induct false
+    else Tactics.new_destruct false
 
 
 let functional_induction with_clean c princl pat =
@@ -77,7 +77,7 @@ let functional_induction with_clean c princl pat =
 	if princ_infos.Tactics.farg_in_concl 
 	then [c] else [] 
       in
-      List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list) 
+      List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list) 
     in 
     let princ' = Some (princ,bindings) in 
     let princ_vars = 
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index fbf72805b7..b975c2e937 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -513,7 +513,7 @@ and intros_with_rewrite_aux : tactic =
 		      Tauto.tauto g
 		  | Case(_,_,v,_) -> 
 		      tclTHENSEQ[
-			h_case (v,Rawterm.NoBindings);
+			h_case false (v,Rawterm.NoBindings);
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ -> 
@@ -550,7 +550,7 @@ let rec reflexivity_with_destruct_cases g =
       match kind_of_term (snd (destApp (pf_concl g))).(2) with 
 	| Case(_,_,v,_) -> 
 	    tclTHENSEQ[
-	      h_case (v,Rawterm.NoBindings);
+	      h_case false (v,Rawterm.NoBindings);
 	      intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases 
 	    ]
@@ -720,7 +720,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	(h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
 	h_intro graph_principle_id;
 	observe_tac "" (tclTHEN_i 
-	  (observe_tac "elim" ((elim (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings)))))
+	  (observe_tac "elim" ((elim false (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings)))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g