Uniformisation des politiques de nommage de NewDestruct sur arguments recursifs et Induction style Hrec; mise en place systeme de traduction automatique; Elim/Case reconnaissent les premisses nommees du but

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

12 files changed, 169 insertions, 111 deletions

diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 2d63e6339d..5918a8b7ee 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1285,7 +1285,7 @@ let rec natural_ntree ig ntree =
 	  | TacAssumption -> natural_trivial ig lh g gs ltree
 	  | TacClear _ -> natural_clear ig lh g gs ltree
 (* Besoin de l'argument de la tactique *)
-	  | TacSimpleInduction (NamedHyp id) -> 
+	  | TacSimpleInduction (NamedHyp id,_) -> 
               natural_induction ig lh g gs ge id ltree false
 	  | TacExtend (_,"InductionIntro",[a]) -> 
               let id=(out_gen wit_ident a) in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index a904753f16..e2460d332d 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -971,7 +971,7 @@ and xlate_tac =
      CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u)
     | TacCase (c1,sl) ->
      CT_casetac (xlate_formula c1, xlate_bindings sl)
-    | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
+    | TacSimpleInduction (h,_) -> CT_induction (xlate_quantified_hypothesis h)
     | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
     | TacCut c -> CT_cut (xlate_formula c)
     | TacLApply c -> CT_use (xlate_formula c)
@@ -1009,12 +1009,12 @@ and xlate_tac =
     | TacClearBody(a::l) -> 
 	CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
     | TacDAuto (a, b) -> CT_dauto(xlate_int_opt a, xlate_int_opt b)
-    | TacNewDestruct(a,b,c) ->
+    | TacNewDestruct(a,b,(c,_)) ->
 	CT_new_destruct
 	  (xlate_int_or_constr a, xlate_using b, 
 	   CT_id_list_list
 	     (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
-    | TacNewInduction(a,b,c) ->
+    | TacNewInduction(a,b,(c,_)) ->
 	CT_new_induction
 	  (xlate_int_or_constr a, xlate_using b, 
 	   CT_id_list_list
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 01b59dcf65..2416b14bd5 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -309,14 +309,14 @@ GEXTEND Gram
       | IDENT "LApply"; c = constr -> TacLApply c
 
       (* Derived basic tactics *)
-      | IDENT "Induction"; h = quantified_hypothesis -> TacSimpleInduction h
+      | IDENT "Induction"; h = quantified_hypothesis -> TacSimpleInduction (h,ref [])
       | IDENT "NewInduction"; c = induction_arg; el = OPT eliminator;
-          ids = with_names -> TacNewInduction (c,el,ids)
+          ids = with_names -> TacNewInduction (c,el,(ids,ref []))
       | IDENT "Double"; IDENT "Induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
       | IDENT "Destruct"; h = quantified_hypothesis -> TacSimpleDestruct h
       | IDENT "NewDestruct"; c = induction_arg; el = OPT eliminator; 
-          ids = with_names -> TacNewDestruct (c,el,ids)
+          ids = with_names -> TacNewDestruct (c,el,(ids,ref []))
       | IDENT "Decompose"; IDENT "Record" ; c = constr -> TacDecomposeAnd c
       | IDENT "Decompose"; IDENT "Sum"; c = constr -> TacDecomposeOr c
       | IDENT "Decompose"; "["; l = LIST1 global_or_ltac_ref; "]"; c = constr
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 8151a8c14f..9ee0041804 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -352,15 +352,15 @@ GEXTEND Gram
 
       (* Derived basic tactics *)
       | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
-          TacSimpleInduction h
+          TacSimpleInduction (h,ref [])
       | IDENT "induction"; c = induction_arg; ids = with_names; 
-	  el = OPT eliminator -> TacNewInduction (c,el,ids)
+	  el = OPT eliminator -> TacNewInduction (c,el,(ids,ref []))
       | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
       | IDENT "simple"; IDENT"destruct"; h = quantified_hypothesis ->
           TacSimpleDestruct h
-      | IDENT "destruct"; c = induction_arg; ids = with_names;
-	  el = OPT eliminator -> TacNewDestruct (c,el,ids)
+      | IDENT "destruct"; c = induction_arg; ids = with_names; 
+	  el = OPT eliminator -> TacNewDestruct (c,el,(ids,ref []))
       | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
       | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
       | IDENT "decompose"; "["; l = LIST1 global; "]"; c = constr
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d7b2cbe449..8a97eb2d0f 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -477,14 +477,14 @@ and pr_atom1 = function
       hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++ 
 	     pr_clauses pr_ident cls)
   (* Derived basic tactics *)
-  | TacSimpleInduction h ->
+  | TacSimpleInduction (h,_) ->
       hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewInduction (h,e,ids) ->
+  | TacNewInduction (h,e,(ids,_)) ->
       hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++
         pr_opt pr_eliminator e ++ pr_with_names ids)
   | TacSimpleDestruct h ->
       hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewDestruct (h,e,ids) ->
+  | TacNewDestruct (h,e,(ids,_)) ->
       hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++
         pr_opt pr_eliminator e ++ pr_with_names ids)
   | TacDoubleInduction (h1,h2) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 57ca81de38..84efdbcac1 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -389,18 +389,18 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacLetTac $id$ $mlexpr_of_constr c$ $cl$ >>
 
   (* Derived basic tactics *)
-  | Tacexpr.TacSimpleInduction h ->
-      <:expr< Tacexpr.TacSimpleInduction $mlexpr_of_quantified_hypothesis h$ >>
+  | Tacexpr.TacSimpleInduction (h,_) ->
+      <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$,ref []) >>
   | Tacexpr.TacNewInduction (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in
-      <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>>
+      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) (fst ids) in
+      <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref [])>>
   | Tacexpr.TacSimpleDestruct h ->
       <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacNewDestruct (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in
-      <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
+      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) (fst ids) in
+      <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref []) >>
 
   (* Context management *)
   | Tacexpr.TacClear l ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 21c2d0c400..743f3cd09d 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -137,12 +137,12 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacInstantiate of int * 'constr * 'id gclause
 
   (* Derived basic tactics *)
-  | TacSimpleInduction of quantified_hypothesis
+  | TacSimpleInduction of (quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref)
   | TacNewInduction of 'constr induction_arg * 'constr with_bindings option
-      * case_intro_pattern_expr
+      * (case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref)
   | TacSimpleDestruct of quantified_hypothesis
   | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
-      * case_intro_pattern_expr 
+      * (case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref)
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index c63bfb84e3..1ea4388746 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -53,14 +53,16 @@ val h_instantiate     : int -> constr -> Tacticals.clause -> tactic
 
 (* Derived basic tactics *)
 
-val h_simple_induction   : quantified_hypothesis -> tactic
+val h_simple_induction   : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic
 val h_simple_destruct    : quantified_hypothesis -> tactic
 val h_new_induction   :
   constr induction_arg -> constr with_bindings option ->
-    intro_pattern_expr list list -> tactic
+  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  -> tactic
 val h_new_destruct    :
   constr induction_arg -> constr with_bindings option -> 
-    intro_pattern_expr list list -> tactic
+  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  -> tactic
 val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f6b05af45c..488e8833cc 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -625,18 +625,18 @@ let rec intern_atomic lf ist x =
   | TacDAuto (n,p) -> TacDAuto (n,p)
 
   (* Derived basic tactics *)
-  | TacSimpleInduction h ->
-      TacSimpleInduction (intern_quantified_hypothesis ist h)
-  | TacNewInduction (c,cbo,ids) ->
+  | TacSimpleInduction (h,ids) ->
+      TacSimpleInduction (intern_quantified_hypothesis ist h,ids)
+  | TacNewInduction (c,cbo,(ids,ids')) ->
       TacNewInduction (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-               intern_case_intro_pattern lf ist ids)
+               (intern_case_intro_pattern lf ist ids,ids'))
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
-  | TacNewDestruct (c,cbo,ids) ->
+  | TacNewDestruct (c,cbo,(ids,ids')) ->
       TacNewDestruct (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-	       intern_case_intro_pattern lf ist ids)
+	       (intern_case_intro_pattern lf ist ids,ids'))
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
       let h2 = intern_quantified_hypothesis ist h2 in
@@ -1633,18 +1633,18 @@ and interp_atomic ist gl = function
   | TacDAuto (n,p) -> Auto.h_dauto (n,p)
 
   (* Derived basic tactics *)
-  | TacSimpleInduction h ->
-      h_simple_induction (interp_quantified_hypothesis ist gl h)
-  | TacNewInduction (c,cbo,ids) ->
+  | TacSimpleInduction (h,ids) ->
+      h_simple_induction (interp_quantified_hypothesis ist gl h,ids)
+  | TacNewInduction (c,cbo,(ids,ids')) ->
       h_new_induction (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (interp_case_intro_pattern ist ids)
+        (interp_case_intro_pattern ist ids,ids')
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist gl h)
-  | TacNewDestruct (c,cbo,ids) -> 
+  | TacNewDestruct (c,cbo,(ids,ids')) -> 
       h_new_destruct (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (interp_case_intro_pattern ist ids)
+        (interp_case_intro_pattern ist ids,ids')
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist gl h1 in
       let h2 = interp_quantified_hypothesis ist gl h2 in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4a864bbf38..b35de35928 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -956,11 +956,16 @@ let find_eliminator c gl =
 let default_elim (c,lbindc) gl = 
   general_elim (c,lbindc) (find_eliminator c gl,NoBindings) gl
 
-let elim (c,lbindc) elim gl =
+let elim_in_context (c,_ as cx) elim gl =
   match elim with
-  | Some (elimc,lbindelimc) -> general_elim (c,lbindc) (elimc,lbindelimc) gl
-  | None -> general_elim (c,lbindc) (find_eliminator c gl,NoBindings) gl 
+  | Some (elimc,lbindelimc) -> general_elim cx (elimc,lbindelimc) gl
+  | None -> general_elim cx (find_eliminator c gl,NoBindings) gl 
 
+let elim (c,lbindc as cx) elim =
+  match kind_of_term c with
+    | Var id when lbindc = NoBindings ->
+	tclTHEN (tclTRY (intros_until_id id)) (elim_in_context cx elim)
+    | _ -> elim_in_context cx elim
 
 (* The simplest elimination tactic, with no substitutions at all. *)
 
@@ -1005,7 +1010,7 @@ let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl =
 
 (* Case analysis tactics *)
 
-let general_case_analysis (c,lbindc) gl =
+let general_case_analysis_in_context (c,lbindc) gl =
   let env = pf_env gl in
   let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   let sigma    = project gl in 
@@ -1014,7 +1019,15 @@ let general_case_analysis (c,lbindc) gl =
   else Indrec.make_case_gen in
   let elim     = case env sigma mind sort in 
   general_elim (c,lbindc) (elim,NoBindings) gl
-    
+
+let general_case_analysis (c,lbindc as cx) =
+  match kind_of_term c with
+    | Var id when lbindc = NoBindings ->
+	tclTHEN (tclTRY (intros_until_id id))
+	(general_case_analysis_in_context cx)
+    | _ ->
+	general_case_analysis_in_context cx
+
 let simplest_case c = general_case_analysis (c,NoBindings)
 
 (*****************************)
@@ -1095,12 +1108,14 @@ let rec first_name_buggy = function
   | IntroWildcard -> None
   | IntroIdentifier id -> Some id
 
-let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
+type elim_arg_kind = RecArg | IndArg | OtherArg
+
+let induct_discharge statuslists destopt avoid' (avoid,ra) (names,force,rnames) gl =
   let avoid = avoid @ avoid' in
   let (lstatus,rstatus) = statuslists in
   let tophyp = ref None in
   let rec peel_tac ra names gl = match ra with
-    | (false,recvarname) :: (true,hyprecname) :: ra' ->
+    | (RecArg,recvarname) :: (IndArg,hyprecname) :: ra' ->
         let recpat,hyprec,names = match names with
           | [] ->
               (IntroIdentifier (fresh_id avoid recvarname gl), 
@@ -1114,15 +1129,53 @@ let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
           | pat1::pat2::names -> (pat1,pat2,names) in
 	(* This is buggy for intro-or-patterns with different first hypnames *)
 	if !tophyp=None then tophyp := first_name_buggy hyprec;
+	rnames := !rnames @ [recpat; hyprec];
         tclTHENLIST
 	  [ intros_pattern destopt [recpat];
 	    intros_pattern None [hyprec];
 	    peel_tac ra' names ] gl
-    | (true,_) :: _ -> anomaly "TODO: non canonical inductive schema"
-    | (false,_) :: ra' ->
+    | (IndArg,hyprecname) :: ra' ->
+	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
+        let pat,names = match names with
+          | [] -> IntroIdentifier (fresh_id avoid hyprecname gl), []
+	  | pat::names -> pat,names in
+	rnames := !rnames @ [pat];
+	tclTHEN (intros_pattern destopt [pat]) (peel_tac ra' names) gl
+    | (RecArg,recvarname) :: ra' ->
+        let introtac,names = match names with
+          | [] -> 
+	      let i = 
+		if !Options.v7 then IntroAvoid avoid 
+		else IntroMustBe (fresh_id avoid recvarname gl)
+	      in
+	      (* For translator *)
+	      let id = fresh_id avoid (default_id gl
+		(match kind_of_term (pf_concl gl) with
+		  | Prod (name,t,_) -> (name,None,t)
+		  | LetIn (name,b,t,_) -> (name,Some b,t) 
+		  | _ -> assert false)) gl in
+	      if Options.do_translate() & id <> fresh_id avoid recvarname gl 
+	      then force := true;
+	      rnames := !rnames @ [IntroIdentifier id];
+	      intro_gen i destopt false, []
+          | pat::names ->
+	      rnames := !rnames @ [pat];
+	      intros_pattern destopt [pat],names in
+	tclTHEN introtac (peel_tac ra' names) gl
+    | (OtherArg,_) :: ra' ->
         let introtac,names = match names with
-          | [] -> intro_gen (IntroAvoid avoid) destopt false, []
-          | pat::names -> intros_pattern destopt [pat],names in
+          | [] -> 
+	      (* For translator *)
+	      let id = fresh_id avoid (default_id gl
+		(match kind_of_term (pf_concl gl) with
+		  | Prod (name,t,_) -> (name,None,t)
+		  | LetIn (name,b,t,_) -> (name,Some b,t) 
+		  | _ -> assert false)) gl in
+	      rnames := !rnames @ [IntroIdentifier id];
+	      intro_gen (IntroAvoid avoid) destopt false, []
+          | pat::names ->
+	      rnames := !rnames @ [pat];
+	      intros_pattern destopt [pat],names in
 	tclTHEN introtac (peel_tac ra' names) gl
     | [] ->
         check_unused_names names;
@@ -1345,42 +1398,6 @@ let is_indhyp p n t =
     | Rel k when p < k & k <= p + n -> true
     | _ -> false
 
-(*
-(* We check that the eliminator has been build by Coq (usual *)
-(* eliminator _ind, _rec or _rect, or eliminator built by Scheme) *)
-let compute_elim_signature_and_roughly_check elimt mind names_info =
-  let (mib,mip) = Global.lookup_inductive mind in
-  let lra = dest_subterms mip.mind_recargs in
-  let nconstr = Array.length mip.mind_consnames in
-  let _,elimt2 = decompose_prod_n mip.mind_nparams elimt in
-  let n = nb_prod elimt2 in
-  let npred = n - nconstr - mip.mind_nrealargs - 1 in
-  let rec check_branch p c ra = match kind_of_term c, ra with
-    | Prod (_,_,c), r :: ra' ->
-	(match dest_recarg r, kind_of_term c with
-	   | Mrec i, Prod (_,t,c) when is_indhyp (p+1) npred t ->
-	       false::true::(check_branch (p+2) c ra')
-	   | _ -> false::(check_branch (p+1) c ra'))
-    | LetIn (_,_,_,c), ra' -> false::(check_branch (p+1) c ra)
-    | _, [] -> []
-    | _ ->
-	error"Not a recursive eliminator: some constructor argument is lacking"
-  in
-  let rec check_elim c n =
-    if n = nconstr then []
-    else match kind_of_term c with
-    | Prod (_,t,c) ->
-	let l = check_branch n t lra.(n) in
-	let p = List.fold_left (fun n b -> if b then n+1 else n) 0 l in
-	let recvarname, hyprecname, avoid = 
-	  make_up_names p (IndRef mind) names_info in
-	let namesign = List.map (fun b -> (b,if b then hyprecname else recvarname)) l in
-	(avoid,namesign) :: (check_elim c (n+1))
-    | _ -> error "Not an eliminator: some constructor case is lacking" in
-  let _,elimt3 = decompose_prod_n npred elimt2 in
-  mip.mind_nparams, IndRef mind, Array.of_list (check_elim elimt3 0)
-*)
-
 let chop_context n l = 
   let rec chop_aux acc = function
     | n, (_,Some _,_ as h :: t) -> chop_aux (h::acc) (n, t)
@@ -1394,6 +1411,8 @@ let error_ind_scheme s =
   let s = if s <> "" then s^" " else s in
   error ("Cannot recognise "^s^"an induction schema")
 
+(* Check that the elimination scheme has a form similar to the 
+   elimination schemes built by Coq *)
 let compute_elim_signature elimt names_info =
   let nparams = ref 0 in
   let hyps,ccl = decompose_prod_assum elimt in
@@ -1419,29 +1438,33 @@ let compute_elim_signature elimt names_info =
   | (na,None,t)::l when isSort (snd (decompose_prod_assum t)) ->
       check_elim (npred+1) l
   | l ->
-    let is_pred n c = match kind_of_term (fst (decompose_app c)) with
-    | Rel q when n < q & q <= n+npred -> true
-    | _ -> false in
+    let is_pred n c = 
+      let hd = fst (decompose_app c) in match kind_of_term hd with
+    | Rel q when n < q & q <= n+npred -> IndArg
+    | _ when hd = indhd -> RecArg
+    | _ -> OtherArg in
     let rec check_branch p c = match kind_of_term c with
     | Prod (_,t,c) -> is_pred p t :: check_branch (p+1) c
-    | LetIn (_,_,_,c) -> false :: check_branch (p+1) c
-    | App (f,_) when is_pred p f -> []
-    | _ when is_pred p c -> []
+    | LetIn (_,_,_,c) -> OtherArg :: check_branch (p+1) c
+(*    | App (f,_) when is_pred p f = IndArg -> []*)
+    | _ when is_pred p c = IndArg -> []
     | _ -> raise Exit in 
     let rec find_branches p = function
     | (_,None,t)::brs ->
 	(match try Some (check_branch p t) with Exit -> None with
 	 | Some l ->
-	     let n = List.fold_left (fun n b -> if b then n+1 else n) 0 l in
+	     let n = List.fold_left
+	       (fun n b -> if (!Options.v7 & b=IndArg) or
+		 (not !Options.v7 & b=RecArg) then n+1 else n) 0 l in
              let recvarname, hyprecname, avoid = make_up_names n indt names_info in
 	     let namesign = List.map
-	       (fun b -> (b,if b then hyprecname else recvarname)) l in
+	       (fun b -> (b,if b=IndArg then hyprecname else recvarname)) l in
 	     (avoid,namesign) :: find_branches (p+1) brs
 	 | None -> error_ind_scheme "the branches of")
     | (_,Some _,_)::_ -> error_ind_scheme "the branches of"
     | [] ->
 	(* Check again conclusion *)
-	let ccl_arg_ok = (is_pred (p + List.length realargs + 1) f) in
+	let ccl_arg_ok = is_pred (p + List.length realargs + 1) f = IndArg in
 	let ind_is_ok = 
 	  list_lastn nrealargs indargs = extended_rel_list 0 realargs in
 	if not (ccl_arg_ok & ind_is_ok) then
@@ -1467,7 +1490,7 @@ let find_elim_signature isrec style elim hyp0 gl =
   let nparams,indref,indsign = compute_elim_signature elimt name_info in
   (elimc,elimt,nparams,indref,indsign)
 
-let induction_from_context isrec elim_info hyp0 names gl =
+let induction_from_context isrec elim_info hyp0 (names,b_rnames) gl =
   (*test suivant sans doute inutile car refait par le letin_tac*)
   if List.mem hyp0 (ids_of_named_context (Global.named_context())) then
     errorlabstrm "induction" 
@@ -1480,6 +1503,12 @@ let induction_from_context isrec elim_info hyp0 names gl =
   let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars env in
   let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
   let names = compute_induction_names (Array.length indsign) names in
+  (* For translator *)
+  let names' = Array.map ref (Array.make (Array.length indsign) []) in
+  let b = ref false in
+  b_rnames := (b,Array.to_list names')::!b_rnames;
+  let names = array_map2 (fun n n' -> (n,b,n')) names names' in
+  (* End translator *)
   let dephyps = List.map (fun (id,_,_) -> id) deps in
   let args =
     List.fold_left
@@ -1549,16 +1578,22 @@ let raw_induct s = tclTHEN (intros_until_id s) (tclLAST_HYP simplest_elim)
 let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim)
 
 (* This was Induction in 6.3 (hybrid form) *)
-let induction_from_context_old_style hyp gl =
+let induction_from_context_old_style hyp b_ids gl =
   let elim_info = find_elim_signature true true None hyp gl in
-  (induction_from_context true elim_info hyp []) gl
-let simple_induct_id hyp =
-  tclORELSE (raw_induct hyp) (induction_from_context_old_style hyp)
+  let x = induction_from_context true elim_info hyp ([],b_ids) gl in
+  (* For translator *) fst (List.hd !b_ids) := true;
+  x
+
+let simple_induct_id hyp b_ids =
+  if !Options.v7 then
+    tclORELSE (raw_induct hyp) (induction_from_context_old_style hyp b_ids)
+  else
+    raw_induct hyp
 let simple_induct_nodep = raw_induct_nodep
 
 let simple_induct = function
-  | NamedHyp id -> simple_induct_id id
-  | AnonHyp n -> simple_induct_nodep n
+  | NamedHyp id,b_ids -> simple_induct_id id b_ids
+  | AnonHyp n,_ -> simple_induct_nodep n
 
 (* Destruction tactics *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 90cb174839..f5c7619947 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -171,12 +171,13 @@ val elim          : constr with_bindings -> constr with_bindings option -> tacti
 val general_elim_in : identifier -> constr * constr bindings ->
                       constr * constr bindings -> tactic
 
-val simple_induct     : quantified_hypothesis -> tactic
+val simple_induct     : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic
 val general_elim_in : identifier -> constr * constr bindings ->
                       constr * constr bindings -> tactic
 
 val new_induct : constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr list list -> tactic
+  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  -> tactic
 
 (*s Case analysis tactics. *)
 
@@ -185,7 +186,8 @@ val simplest_case         : constr -> tactic
 
 val simple_destruct          : quantified_hypothesis -> tactic
 val new_destruct : constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr list list -> tactic
+  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)
 
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 72d4a56082..9ab1747b07 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -318,6 +318,15 @@ let pr_seq_body pr tl =
         prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
         str " ]")
 
+let duplicate force pr = function
+  | [] -> pr (ref false,[])
+  | [x] -> pr x
+  | l ->
+      if List.exists (fun (b,ids) -> !b) l & (force or
+	 List.exists (fun (_,ids) -> ids <> (snd (List.hd l))) (List.tl l))
+      then pr_seq_body pr (List.rev l)
+      else pr (ref false,[])
+
 let pr_hintbases = function
   | None -> spc () ++ str "with *"
   | Some [] -> mt ()
@@ -491,18 +500,28 @@ and pr_atom1 env = function
                     pr_lconstrarg env c ++ str ")" ++ 
 		    pr_clauses pr_ident cls))
   (* Derived basic tactics *)
-  | TacSimpleInduction h ->
+  | TacSimpleInduction (h,l) ->
+      if List.exists (fun (pp,_) -> !pp) !l then
+      duplicate true (fun (_,ids) ->
+      hov 1 (str "induction" ++ spc () ++ pr_arg pr_quantified_hypothesis h ++ 
+      pr_with_names (List.map (fun x -> !x) ids))) !l
+      else
       hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewInduction (h,e,ids) ->
+  | TacNewInduction (h,e,(ids,l))
+  | TacNewDestruct (h,(Some _ as e),(ids,l)) ->
+      duplicate false (fun (pp,ids') ->
       hov 1 (str "induction" ++ spc () ++
-             pr_induction_arg (pr_constr env) h ++ pr_with_names ids ++
-             pr_opt (pr_eliminator env) e)
+             pr_induction_arg (pr_constr env) h ++ 
+      pr_with_names (if !pp then List.map (fun x -> !x) ids' else ids) ++
+             pr_opt (pr_eliminator env) e)) !l
   | TacSimpleDestruct h ->
       hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewDestruct (h,e,ids) ->
+  | TacNewDestruct (h,None,(ids,l)) ->
+      duplicate false (fun (pp,ids') ->
       hov 1 (str "destruct" ++ spc () ++
-             pr_induction_arg (pr_constr env) h ++ pr_with_names ids ++
-             pr_opt (pr_eliminator env) e)
+             pr_induction_arg (pr_constr env) h ++ 
+      pr_with_names (if !pp then List.map (fun x -> !x) ids' else ids)
+(*      ++ pr_opt (pr_eliminator env) e*) )) !l
   | TacDoubleInduction (h1,h2) ->
       hov 1
         (str "double induction" ++