changed the decomposition of an induction scheme

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

2 files changed, 209 insertions, 229 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b21ffd96d..c621f0200 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -725,7 +725,7 @@ let general_elim c e ?(allow_K=true) =
 
 let find_eliminator c gl =
   let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  Indrec.lookup_eliminator ind (elimination_sort_of_goal gl)
+  lookup_eliminator ind (elimination_sort_of_goal gl)
 
 let default_elim (c,_ as cx) gl = 
   general_elim cx (find_eliminator c gl,NoBindings) gl
@@ -1384,12 +1384,19 @@ let make_base n id =
     (* digits *)
     id_of_string (atompart_of_id (make_ident (string_of_id id) (Some 0)))
 
-let make_up_names n ind cname = 
+(* Builds tw different names from an optional inductive type and a
+   number, also deals with a list of names to avoid. If the inductive
+   type is None, then hyprecname is HIi where i is a number. *)
+let make_up_names n ind_opt cname = 
   let is_hyp = atompart_of_id cname = "H" in
   let base = string_of_id (make_base n cname) in
-  let hyprecname =
-    add_prefix "IH"
-      (make_base n (if is_hyp then Nametab.id_of_global ind else cname)) in
+  let base_ind = 
+    if is_hyp then 
+      match ind_opt with
+	| None -> id_of_string ""
+	| Some ind_id -> Nametab.id_of_global ind_id 
+    else cname in
+  let hyprecname = add_prefix "IH" (make_base n base_ind) in
   let avoid =
     if n=1 (* Only one recursive argument *) or n=0 then []
     else
@@ -1567,222 +1574,193 @@ type elim_scheme = {
 				     if HI is in premisses, None otherwise *)
   concl: types;            (* Qi x1...xni HI (f...), HI and (f...) 
 			      are optional and mutually exclusive *)
-  indarg_in_concl:bool;    (* true if HI appears at the end of conclusion *)
-  farg_in_concl:bool;      (* true if (f...) appears at the end of conclusion *)
+  indarg_in_concl: bool;   (* true if HI appears at the end of conclusion *)
+  farg_in_concl: bool;     (* true if (f...) appears at the end of conclusion *)
 }
 
+let empty_scheme = 
+  { 
+    elimc = mkProp,NoBindings;
+    elimt = mkProp;
+    indref = None;
+    params = [];
+    nparams = 0;
+    predicates = [];
+    branches = [];
+    args = [];
+    nargs = 0;
+    indarg = None;
+    concl = mkProp;
+    indarg_in_concl = false;
+    farg_in_concl = false;
+  }
+
 exception NoLastArg
 exception NoLastArgCcl
 
+(* Builds an elim_scheme frome its type and calling form (const+binding) We
+   first separate branches.  We obtain branches, hyps before (params + preds),
+   hyps after (args <+ indarg if present>) and conclusion.  Then we proceed as
+   follows:
+   
+   - separate parameters and predicates in params_preds. For that we build: 
+ forall (x1:Ti_1)(xni:Ti_ni) (HI:I prm1..prmp x1...xni), DUMMY x1...xni HI/farg
+                             ^^^^^^^^^^^^^^^^^^^^^^^^^                  ^^^^^^^
+                                       optional                           opt
+     Free rels appearing in this term are parameters (branches should not
+     appear, and the only predicate would have been Qi but we replaced it by
+     DUMMY). We guess this heuristic catches all params.  TODO: generalize to
+     the case where args are merged with branches (?) and/or where several
+     predicates are cited in the conclusion.
+
+   - finish to fill in the elim_scheme: indarg/farg/args and finally indref. *)
 let compute_elim_sig elimc elimt =
-  (* We first separate branches (easily identified because they have a
-     special form AND correpsponding rels do not appear in the
-     principle). We obtain branches, what was found before branches
-     (params_preds), what was found after branches (args_indargs) and
-     conclusion. Two operations remain: separate parameters from
-     predicates and separate main indarg from args if there is one. *)
   let params_preds,branches,args_indargs,conclusion = 
     decompose_paramspred_branch_args elimt in
-
-  (* ccl is conclusion where Qi (that is rel <something>) is replaced by a
-     constant to avoid it being counted as an arg or parameter in the following. *)
+  
   let ccl = exchange_hd_app (mkVar (id_of_string "__QI_DUMMY__")) conclusion in
-  (* Now we want to know which hyps remaining are predicates and which
-     are parameters. We rebuild:
-      
-     forall (x1:Ti_1) (xni:Ti_ni) (HI:I prm1..prmp x1...xni), DUMMY x1...xni HI
-                                  ^^^^^^^^^^^^^^^^^^^^^^^^^                  ^^
-                                          optional                           opt
-     Free rels appearing in this term are parameters (branches and
-     predicate should not appear). We catch all of them if HI is
-     present. In this case the number of parameters is the number of
-     free rels. Otherwise (principle generated by functional induction
-     or by hand) WE GUESS that all parameters appear in Ti_js, IS THAT
-     TRUE??.  TODO: if we want to generalize to the case where args
-     are merged with branches (?) and/or where several predicates are
-     cited in the conclusion, we should do something more precise than
-     just counting free rels. *)
   let concl_with_args = it_mkProd_or_LetIn ccl args_indargs in  
   let nparams = Intset.cardinal (free_rels concl_with_args) in
   let preds,params = cut_list (List.length params_preds - nparams) params_preds in
-  let nargs_indargs = List.length args_indargs in  
-
-  (* indarg is the inductive argument if it exists. dep is true if indarg is
-     present AND appears in the conclusion. farg_in_concl is true if (f...) 
-     appears at the end of conclusion. dep and farg_in_concl cannot be both
-     true.
-
-     If it exists it is the first element of hyps. To know if the
-     first elmt of hyps is an inductive arg, we check if it is an
-     inductive type applied to the right number of terms
-     (nparams-1+narg). *)
-  let args,indarg,dep,farg_in_concl = 
-    try (* last_arg_ccl is the last argument of the conclusion if present *)
-      let last_arg_ccl = 
-	try List.hd (List.rev (snd (decompose_app ccl))) 
-	with Failure "hd" -> raise NoLastArgCcl in
-      if isApp last_arg_ccl  (* if last arg of ccl is an application *)
-      then args_indargs , None , false , true (* then this a functional ind principle *)
-      else (* otherwise it is an inductive principle with no (f...) *)
-	(* ccl avoids the pathological where rel 1 is present but
-	   corresponds to a predicate *)
-	let last_arg = 
-	  try List.hd args_indargs 
-	  with Failure "hd" -> raise NoLastArg in
-	match last_arg with
-	  | hiname,Some _,hi -> error "cannot recognize an induction schema"
-	  | hiname,None,hi -> 
-	      let hi_ind, hi_args = decompose_app hi in
-	      let hi_is_ind = 
-		match kind_of_term hi_ind with
-		  | Ind (mind,_)  -> true
-		  | _ -> false in
-	      let hi_args_enough = 
-		List.length hi_args = List.length params + nargs_indargs -1 in
-	      if hi_is_ind & hi_args_enough 
-	      then List.tl args_indargs , Some last_arg , occur_rel 1 ccl , false
-	      else args_indargs , None , false , false
-    with 
-	NoLastArgCcl -> 
-	  List.tl args_indargs , Some (List.hd args_indargs) , false , false
-      | NoLastArg -> args_indargs , None , false , false
-      | Failure s -> error "cannot recognize an induction schema" in
-
-  let indref = 
-    match indarg with
-      | None -> (* No indarg: we take the last arg or param *)
-	  let largs = args @ params in
-	  if List.length largs = 0 then None 
- 	  else
-	    let _,_,typ_fstarg = List.hd largs in
-	    let indhd,indargs = decompose_app typ_fstarg in
-	    (try Some (global_of_constr indhd)
-	    with _ -> error "Cannot find the inductive type of the inductive schema")
-      | Some ( _,indbody,ind) -> 
-	  (if indbody <> None then error "Cannot recognise an induction scheme";
+
+  (* A first approximation, further anlysis will tweak it *)
+  let res = ref { empty_scheme with
+    (* This fields are ok: *)
+    elimc = elimc; elimt = elimt; concl = conclusion;
+    predicates = preds; branches = branches; 
+    farg_in_concl = (try isApp (last_arg ccl) with _ -> false);
+    params = params; nparams = nparams; 
+    (* This fields (+ indarg + indref + indarg_in_concl + farg_in_concl)
+       are approximate at this point: *)
+    args = args_indargs; nargs = List.length args_indargs; } in
+  try 
+    (* Order of following tests is important. Each of them exits if successful. *)
+    (* 1- First see if (f x...) is in the conclusion. *)
+    if !res.farg_in_concl 
+    then begin
+      res := { !res with
+	indarg = None;
+	indarg_in_concl = false; farg_in_concl = true };
+      raise Exit
+    end;
+    (* 2- If no args_indargs then no indarg (indarg cannot be a parameter). *)
+    if !res.nargs=0 then raise Exit;
+    (* 3- Look at last arg: is it the indarg? *)
+    ignore (
+      match List.hd args_indargs with
+	| hiname,Some _,hi -> error "cannot recognize an induction schema"
+	| hiname,None,hi -> 
+	    let hi_ind, hi_args = decompose_app hi in
+	    let hi_is_ind = (* hi est d'un type inductif *)
+	      match kind_of_term hi_ind with | Ind (mind,_)  -> true | _ -> false in
+	    let hi_args_enough = (* hi a le bon nbre d'arguments *)
+	      List.length hi_args = List.length params + !res.nargs -1 in
+	    (* FIXME: Ces deux tests ne sont pas suffisants. *)
+	    if not (hi_is_ind & hi_args_enough)
+	    then raise Exit (* No indarg, args and params unchanged *)
+	    else (* Last arg is the indarg *)
+	      res := {!res with
+		indarg = Some (List.hd !res.args);
+		indarg_in_concl = occur_rel 1 ccl;
+		args = List.tl !res.args;
+		nargs = !res.nargs - 1;
+	      };
+	    raise Exit);
+    raise Exit
+  with Exit -> (* Ending by computing indrev: *)
+    match !res.indarg with
+      | None -> !res (* No indref *)
+      | Some ( _,Some _,_) -> error "Cannot recognise an induction scheme"
+      | Some ( _,None,ind) -> 
 	  let indhd,indargs = decompose_app ind in
-	  try Some (global_of_constr indhd)
-	  with _ -> error "Cannot find the inductive type of the inductive schema") in
-  
-  let elimscheme = {
-    elimc=elimc;
-    elimt=elimt;
-    indref = indref;
-    params = params;
-    nparams = List.length params;
-    predicates = preds;
-    branches = branches;
-    args = args;
-    nargs = List.length args;
-    indarg = indarg;
-    concl = conclusion;
-    indarg_in_concl = dep;
-    farg_in_concl = farg_in_concl;
-  }
-  in
-  elimscheme
+	  try {!res with indref = Some (global_of_constr indhd) }
+	  with _ -> error "Cannot find the inductive type of the inductive schema";;
 
 (* Check that the elimination scheme has a form similar to the 
-   elimination schemes built by Coq *)
+   elimination schemes built by Coq. Schemes may have the standard
+   form computed from an inductive type OR (feb. 2006) a non standard
+   form. That is: with no main induction argument and with an optional
+   extra final argument of the form (f x y ...) in the conclusion. In
+   the non standard case, naming of generated hypos is slightly
+   different. *)
 let compute_elim_signature elimc elimt names_info =
   let scheme = compute_elim_sig elimc elimt in
-  let revhyps2 = List.rev (scheme.branches@scheme.predicates) in
   let f,l = decompose_app scheme.concl in
-  let indt = 
-    match scheme.indref with
-    | None -> VarRef (id_of_string "DUMMY")
-    | Some x -> x in
-  (match scheme.indarg with
-    | Some (_,Some _,_) -> error "strange letin, cannot recognise an induction schema"
-    | _ -> ());
-  (* Vérifier que les argument de Qi sont bien les xi. *)
+  (* Vérifier que les arguments de Qi sont bien les xi. *)
   match scheme.indarg with
-    | None -> 
-	let rec check_elim npred = 
-	  function
-	  | (na,None,t)::l when isSort (snd (decompose_prod_assum t)) ->
-	      check_elim (npred+1) l
-	  | l ->
-	      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
-		  | _ -> OtherArg in(* No rec arg *)
-	      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) -> 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=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=IndArg then hyprecname else recvarname)) l in
-			  (avoid,namesign) :: find_branches (p+1) brs
-		      | None -> error_ind_scheme "the correct branches of")
-		| (_,Some _,_)::_ -> error_ind_scheme "the branches (without letins) of"
-		| [] ->
-		    (* Check again conclusion *)
-		    (* let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f = IndArg in
-		    let ind_is_ok = 
-		      list_lastn scheme.nargs indargs = extended_rel_list 0 scheme.args in
-		    if not (ccl_arg_ok & ind_is_ok) then
-		      error "Cannot recognize the conclusion of an induction schema2";
-		    *)
-		    [] in
-	      find_branches 0 l in
-	(Array.of_list (check_elim 0 revhyps2)),scheme
-
+    | Some (_,Some _,_) -> error "strange letin, cannot recognize an induction schema"
+    | None -> (* Non standard scheme *)
+	let npred = List.length scheme.predicates 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
+	    | _ -> 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) -> OtherArg :: check_branch (p+1) c
+	    | _ when is_pred p c = IndArg -> []
+	    | _ -> raise Exit in 
+	let rec find_branches p lbrch = 
+	  match lbrch with
+	    | (_,None,t)::brs ->
+		(try
+		  let lchck_brch = check_branch p t in
+		  let n = List.fold_left 
+		    (fun n b -> if b=RecArg then n+1 else n) 0 lchck_brch in
+		  let recvarname, hyprecname, avoid = 
+		    make_up_names n scheme.indref names_info in
+		  let namesign = 
+		    List.map (fun b -> (b,if b=IndArg then hyprecname else recvarname))
+		      lchck_brch in
+		  (avoid,namesign) :: find_branches (p+1) brs
+		with Exit-> error_ind_scheme "the branches of")
+	    | (_,Some _,_)::_ -> error_ind_scheme "the branches of"
+	    | [] -> [] in
+	let indsign = Array.of_list (find_branches 0 (List.rev scheme.branches)) in
+	indsign,scheme	
 	
-    | Some ( _,indbody,ind) -> 
-	if indbody <> None then error "Cannot recognise an induction scheme";
+    | Some ( _,None,ind) -> (* Standard scheme from an inductive type *)
 	let indhd,indargs = decompose_app ind in
-	let rec check_elim npred = function
-	  | (na,None,t)::l when isSort (snd (decompose_prod_assum t)) ->
-	      check_elim (npred+1) l
-	  | l ->
-	      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) -> 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=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=IndArg then hyprecname else recvarname)) l in
-			  (avoid,namesign) :: find_branches (p+1) brs
-		      | None -> error_ind_scheme "the correct branches of")
-		| (_,Some _,_)::_ -> error_ind_scheme "the branches (without letins) of"
-		| [] ->
-		    (* Check again conclusion *)
-		    let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f = IndArg in
-		    let ind_is_ok = 
-		      list_lastn scheme.nargs indargs 
-		      = extended_rel_list 0 scheme.args in
-		    if not (ccl_arg_ok & ind_is_ok) then
-		      error "Cannot recognize the conclusion of an induction schema";
-		    [] in
-	      find_branches 0 l in
-	(Array.of_list (check_elim 0 revhyps2)),scheme
+	let npred = List.length scheme.predicates 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) -> OtherArg :: check_branch (p+1) c
+	  | _ when is_pred p c = IndArg -> []
+	  | _ -> raise Exit in 
+	let rec find_branches p lbrch =
+	  match lbrch with
+	    | (_,None,t)::brs ->
+		(try
+		  let lchck_brch = check_branch p t in
+		  let n = List.fold_left 
+		    (fun n b -> if b=RecArg then n+1 else n) 0 lchck_brch in
+		  let recvarname, hyprecname, avoid = 
+		    make_up_names n scheme.indref names_info in
+		  let namesign = 
+		    List.map (fun b -> (b,if b=IndArg then hyprecname else recvarname))
+		      lchck_brch in
+		  (avoid,namesign) :: find_branches (p+1) brs
+		with Exit -> error_ind_scheme "the branches of")
+	    | (_,Some _,_)::_ -> error_ind_scheme "the branches of"
+	    | [] ->
+		(* Check again conclusion *)
+
+		let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f = IndArg in
+		let ind_is_ok = 
+		  list_lastn scheme.nargs indargs 
+		  = extended_rel_list 0 scheme.args in
+		if not (ccl_arg_ok & ind_is_ok) then
+		  error "Cannot recognize the conclusion of an induction schema";
+		[] 
+	in
+	let indsign = Array.of_list (find_branches 0 (List.rev scheme.branches)) in
+	indsign,scheme
 
 
 let find_elim_signature isrec elim hyp0 gl =
@@ -1792,8 +1770,8 @@ let find_elim_signature isrec elim hyp0 gl =
 	let mind,_ = pf_reduce_to_quantified_ind gl tmptyp0 in
 	let s = elimination_sort_of_goal gl in
 	let elimc =
-	  if isrec then Indrec.lookup_eliminator mind s
-	  else pf_apply Indrec.make_case_gen gl mind s in
+	  if isrec then lookup_eliminator mind s
+	  else pf_apply make_case_gen gl mind s in
 	let elimt = pf_type_of gl elimc in
 	((elimc, NoBindings), elimt)
     | Some (elimc,lbind as e) -> 
@@ -1808,16 +1786,18 @@ let induction_from_context isrec elim_info hyp0 names gl =
     errorlabstrm "induction" 
       (str "Cannot generalize a global variable");
   let indsign,scheme = elim_info in
+
   let indref = match scheme.indref with | None -> assert false | Some x -> x in
   let tmptyp0 =	pf_get_hyp_typ gl hyp0 in
   let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
+
   let env = pf_env gl in
   let indvars = find_atomic_param_of_ind scheme.nparams (snd (decompose_prod typ0)) in
-  let (statlists,lhyp0,indhyps,deps) = cook_sign (Some hyp0) indvars env in
+  let statlists,lhyp0,indhyps,deps = cook_sign (Some 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
   let dephyps = List.map (fun (id,_,_) -> id) deps in
-  let args =
+  let deps_cstr =
     List.fold_left
       (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in
 
@@ -1830,7 +1810,7 @@ let induction_from_context isrec elim_info hyp0 names gl =
      "ind_rec ... (hyp0 ?)", les buts correspondant ŕ des arguments de
      hyp0 sont maintenant ŕ la fin et c'est tclTHENFIRSTn qui marche !!! *)
   tclTHENLIST
-    [ if deps = [] then tclIDTAC else apply_type tmpcl args;
+    [ if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr;
       thin dephyps;
       (if isrec then tclTHENFIRSTn else tclTHENLASTn)
        	(tclTHENLIST
@@ -1901,32 +1881,32 @@ let induction_tac_felim indvars (elimc,lbindelimc) elimt scheme gl =
   (* elimclause' is built from elimclause by instanciating all args and params. *)
   let elimclause' = recolle_clenv scheme indvars elimclause gl in
   (* one last resolution (useless?) *)
-  let resolved = Clenv.clenv_unique_resolver true elimclause' gl in
-  Clenvtac.clenv_refine resolved gl
+  let resolved = clenv_unique_resolver true elimclause' gl in
+  clenv_refine resolved gl
 
-(* induction with several induction arguments, main differences with
+(* Induction with several induction arguments, main differences with
    induction_from_context is that there is no main induction argument,
    so we chose one to be the positioning reference. On the other hand,
    all args and params must be given, so we help a bit the unifier by
    making the "pattern" by hand before calling induction_tac_felim
    FIXME: REUNIF AVEC induction_tac_felim? *)
-let induction_from_context_noind isrec elim_info lid names gl =
+let induction_from_context_l isrec elim_info lid names gl =
   let indsign,scheme = elim_info in
   (* hyp0 is the first element of the list of variables on which to
      induct. It is most probably the first of them appearing in the
      context. So it seems to be a good value for hyp0, which is used
      for re-introducing hyps at the right place afterward. *)
   let env = pf_env gl in
-  let hyp0,indvars,lparam_part = 
-  match lid with
-    | []  -> anomaly "induction_from_context_noind"
-    | e::l -> 
-	let nargs_without_indarg = 
-	  scheme.nargs - 1 
-	  + (if scheme.farg_in_concl then 1 else 0) 
-	  + (if scheme.indarg <> None then 1 else 0) in
-	let ivs,lp = cut_list nargs_without_indarg l in
-	e, ivs, lp in
+  let hyp0,indvars,lid_params = 
+    match lid with
+      | []  -> anomaly "induction_from_context_l"
+      | e::l -> 
+	  let nargs_without_indarg = 
+	    scheme.nargs - 1
+	    + (if scheme.farg_in_concl then 1 else 0) 
+	    + (if scheme.indarg <> None then 1 else 0) in
+	  let ivs,lp = cut_list nargs_without_indarg l in
+	  e, ivs, lp in
   let statlists,lhyp0,indhyps,deps = cook_sign None (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
@@ -1936,12 +1916,12 @@ let induction_from_context_noind isrec elim_info lid names gl =
       (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in
   (* terms to patternify we must patternify indarg or farg if present in concl *)
   let lid_in_pattern = 
-    if scheme.indarg_in_concl || scheme.farg_in_concl then hyp0::indvars 
-    else indvars in
+    if scheme.indarg <> None & not scheme.indarg_in_concl then indvars
+    else hyp0::indvars in
   let lidcstr = List.map (fun x -> mkVar x) lid_in_pattern in
   let realindvars = (* hyp0 is a real induction arg if it is not the
 		       farg in the conclusion of the induction scheme *)
-    lparam_part @ (if scheme.farg_in_concl then indvars else hyp0::indvars) in
+    lid_params @ (if scheme.farg_in_concl then indvars else hyp0::indvars) in
   (* Magistral effet de bord: comme dans induction_from_context. *)
   tclTHENLIST
     [ 
@@ -1958,7 +1938,6 @@ let induction_from_context_noind isrec elim_info lid names gl =
 	     functional one). *)
 	  induction_tac_felim realindvars scheme.elimc scheme.elimt scheme;
           tclTRY (thin (List.rev (indhyps)));
-	  tclTRY (thin [hyp0]) 
 	])
 	(array_map2 
 	  (induct_discharge statlists lhyp0 (List.rev dephyps)) indsign names)
@@ -1973,7 +1952,7 @@ let induction_with_atomization_of_ind_arg isrec elim names hyp0 gl =
   if scheme.indarg = None then (* This is not a standard induction scheme (the
 				  argument is probably a parameter) So try the
 				  more general induction mechanism. *)
-    induction_from_context_noind isrec elim_info [hyp0] names gl
+    induction_from_context_l isrec elim_info [hyp0] names gl
   else
     let indref = match scheme.indref with | None -> assert false | Some x -> x in
     tclTHEN
@@ -1994,7 +1973,7 @@ let induction_without_atomization isrec elim names lid gl =
   let nlid = List.length lid in
   if nlid <> awaited_nargs
   then error "Not the right number of induction arguments"
-  else induction_from_context_noind isrec elim_info lid names gl
+  else induction_from_context_l isrec elim_info lid names gl
 
 let new_induct_gen isrec elim names c gl =
   match kind_of_term c with
@@ -2124,13 +2103,13 @@ let elim_scheme_type elim t gl =
 
 let elim_type t gl =
   let (ind,t) = pf_reduce_to_atomic_ind gl t in
-  let elimc = Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in
+  let elimc = lookup_eliminator ind (elimination_sort_of_goal gl) in
   elim_scheme_type elimc t gl
 
 let case_type t gl =
   let (ind,t) = pf_reduce_to_atomic_ind gl t in
   let env = pf_env gl in
-  let elimc = Indrec.make_case_gen env (project gl) ind (elimination_sort_of_goal gl) in 
+  let elimc = make_case_gen env (project gl) ind (elimination_sort_of_goal gl) in 
   elim_scheme_type elimc t gl
 
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 1b8e67842..eef6b21b7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -167,6 +167,7 @@ val cut_and_apply         : constr -> tactic
 
 (*s Elimination tactics. *)
 
+
 (*
    The general form of an induction principle is the following:
    
@@ -206,8 +207,8 @@ type elim_scheme = {
 				     if HI is in premisses, None otherwise *)
   concl: types;            (* Qi x1...xni HI (f...), HI and (f...) 
 			      are optional and mutually exclusive *)
-  indarg_in_concl:bool;    (* true if HI appears at the end of conclusion *)
-  farg_in_concl:bool;      (* true if (f...) appears at the end of conclusion *)
+  indarg_in_concl: bool;   (* true if HI appears at the end of conclusion *)
+  farg_in_concl: bool;     (* true if (f...) appears at the end of conclusion *)
 }
 
 val compute_elim_sig : Term.constr * constr Rawterm.bindings -> types -> elim_scheme