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

6 files changed, 22 insertions, 17 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
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index d96b639531..be99bdde0a 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -175,7 +175,7 @@ let make_pbp_atomic_tactic = function
   | PbpElim (hyp_name, names) ->
       let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
       TacAtom
-	(zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None))
+	(zz, TacElim (false,(make_var hyp_name,ExplicitBindings bind),None))
   | PbpTryClear l -> 
       TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l)))
   | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));;
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index ab4da05e32..e3f6572020 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1208,11 +1208,12 @@ let rec natural_ntree ig ntree =
 	  | TacExtend (_,"CutIntro",[a]) ->
 	      let _c = out_gen wit_constr a in
 	      natural_cutintro ig lh g gs a ltree
-	  | TacCase (c,_) -> natural_case ig lh g gs ge (snd c) ltree false
+	  | TacCase (_,(c,_)) -> natural_case ig lh g gs ge (snd c) ltree false
 	  | TacExtend (_,"CaseIntro",[a]) ->
 	      let c = out_gen wit_constr a in
 	      natural_case ig lh g gs ge c ltree true
-	  | TacElim ((c,_),_) -> natural_elim ig lh g gs ge (snd c) ltree false
+	  | TacElim (_,(c,_),_) ->
+	      natural_elim ig lh g gs ge (snd c) ltree false
 	  | TacExtend (_,"ElimIntro",[a]) ->
 	      let c = out_gen wit_constr a in
 	      natural_elim ig lh g gs ge c ltree true
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index e2ba05348c..4f98b7396b 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -663,7 +663,8 @@ let xlate_largs_to_id_opt largs =
     | _ -> assert false;;
 
 let xlate_int_or_constr = function
-    ElimOnConstr a -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a)
+    ElimOnConstr (a,NoBindings) -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a)
+  | ElimOnConstr _ -> xlate_error "TODO: ElimOnConstr with bindings"
   | ElimOnIdent(_,i) ->
       CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
       	(CT_coerce_ID_to_ID_OR_INT(xlate_ident i))
@@ -1162,10 +1163,13 @@ and xlate_tac =
 	CT_generalize_dependent (xlate_formula c)
     | TacElimType c -> CT_elim_type (xlate_formula c)
     | TacCaseType c -> CT_case_type (xlate_formula c)
-    | TacElim ((c1,sl), u) ->
+    | TacElim (false,(c1,sl), u) ->
      CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u)
-    | TacCase (c1,sl) ->
+    | TacCase (false,(c1,sl)) ->
      CT_casetac (xlate_formula c1, xlate_bindings sl)
+    | TacElim (true,_,_) | TacCase (true,_)
+    | TacNewDestruct (true,_,_,_) | TacNewInduction (true,_,_,_) ->
+	xlate_error "TODO: eelim, ecase, edestruct, einduction"
     | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
     | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
     | TacCut c -> CT_cut (xlate_formula c)
@@ -1207,12 +1211,12 @@ and xlate_tac =
 	CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
     | TacDAuto (a, b, _) ->
 	xlate_error "TODO: dauto using"
-    | TacNewDestruct(a,b,c) ->
-	CT_new_destruct (* Julien F. : est-ce correct *)
+    | TacNewDestruct(false,a,b,c) ->
+	CT_new_destruct
 	  (List.map  xlate_int_or_constr a, xlate_using b, 
 	   xlate_with_names c)
-    | TacNewInduction(a,b,c) ->
-	CT_new_induction (* Pierre C. : est-ce correct *)
+    | TacNewInduction(false,a,b,c) ->
+	CT_new_induction
 	  (List.map xlate_int_or_constr a, xlate_using b,
 	   xlate_with_names c)
     (*| TacInstantiate (a, b, cl) ->