Bugs, nettoyage, et améliorations diverses

- vérification de la cohérence des ident pour éviter une option -R
  avec des noms non parsables (la vérification est faite dans
  id_of_string ce qui est très exigeant; faudrait-il une solution plus
  souple ?)
- correction message d'erreur inapproprié dans le apply qui descend dans les 
  conjonctions
- nettoyage autour de l'échec en présence de métas dans le prim_refiner
- nouveau message d'erreur quand des variables ne peuvent être instanciées
- quelques simplifications et davantage de robustesse dans inversion
- factorisation du code de constructor and co avec celui de econstructor and co

Documentation des tactiques
- edestruct/einduction/ecase/eelim et nouveautés apply
- nouvelle sémantique des intropatterns disjonctifs et documentation des
  pattern -> et <-
- relecture de certaines parties du chapitre tactique


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

11 files changed, 126 insertions, 186 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 9b0bb188b9..5388bf2073 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1138,7 +1138,7 @@ let declare_instance_trans binders a aeq n lemma =
   in anew_instance binders instance 
        [((dummy_loc,id_of_string "transitivity"),[],lemma)]
 
-let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None)) 
+let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor (false,None)))
 
 let declare_relation ?(binders=[]) a aeq n refl symm trans = 
   init_setoid ();
@@ -1421,7 +1421,8 @@ let check_evar_map_of_evars_defs evd =
   Evd.Metaset.iter
    (fun m ->
      if Evd.meta_defined evd m then () else
-      raise (Logic.RefinerError (Logic.OccurMetaGoal rebus)))
+      raise
+	(Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m])))
  in
   List.iter
    (fun (_,binding) ->
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 74d6f9ccc1..5c59e8244a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -55,69 +55,6 @@ let registered_e_assumption gl =
   tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) 
               (pf_ids_of_hyps gl)) gl
 
-let e_constructor_tac boundopt i lbind gl = 
-    let cl = pf_concl gl in 
-  let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in 
-  let nconstr =
-    Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
-  if i=0 then error "The constructors are numbered starting from 1";
-  if i > nconstr then error "Not enough constructors";
-  begin match boundopt with 
-    | Some expctdnum -> 
-        if expctdnum <> nconstr then 
-	  error "Not the expected number of constructors"
-    | None -> ()
-  end;
-  let cons = mkConstruct (ith_constructor_of_inductive mind i) in
-  let apply_tac = eapply_with_ebindings (cons,lbind) in
-  (tclTHENLIST [convert_concl_no_check redcl DEFAULTcast
-; intros; apply_tac]) gl
-
-let e_one_constructor i = e_constructor_tac None i
-
-let e_any_constructor tacopt gl =
-  let t = match tacopt with None -> tclIDTAC | Some t -> t in
-  let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in
-  let nconstr =
-    Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
-  if nconstr = 0 then error "The type has no constructors";
-  tclFIRST (List.map (fun i -> tclTHEN (e_one_constructor i NoBindings) t) 
-              (interval 1 nconstr)) gl
-
-let e_left = e_constructor_tac (Some 2) 1
-
-let e_right = e_constructor_tac (Some 2) 2
-
-let e_split = e_constructor_tac (Some 1) 1
-
-(* This automatically define h_econstructor (among other things) *)
-TACTIC EXTEND econstructor
-  [ "econstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ]
-| [ "econstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ]
-| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (Option.map Tacinterp.eval_tactic t) ] 
-      END
-
-TACTIC EXTEND eleft
-  [ "eleft" "with" bindings(l) ] -> [e_left l]
-| [ "eleft"] -> [e_left NoBindings]
-END
-
-TACTIC EXTEND eright
-  [ "eright" "with" bindings(l) ] -> [e_right l]
-| [ "eright" ] -> [e_right NoBindings]
-END
-
-TACTIC EXTEND esplit
-  [ "esplit" "with" bindings(l) ] -> [e_split l]
-| [ "esplit"] -> [e_split NoBindings]
-END
-
-
-TACTIC EXTEND eexists
-  [ "eexists" bindings(l) ] -> [e_split l]
-END
-
-
 (************************************************************************)
 (*   PROLOG tactic                                                      *)
 (************************************************************************)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 18263127be..0cb3142013 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -97,18 +97,18 @@ let h_rename l =
 let h_revert l = abstract_tactic (TacRevert l) (revert l)
 
 (* Constructors *)
-let h_left l    = abstract_tactic (TacLeft l) (left_with_ebindings l)
-let h_right l   = abstract_tactic (TacLeft l) (right_with_ebindings l)
-let h_split l   = abstract_tactic (TacSplit (false,l)) (split_with_ebindings l)
-(* Moved to tacinterp because of dependence in Tacinterp.interp
+let h_left ev l  = abstract_tactic (TacLeft (ev,l)) (left_with_ebindings ev l)
+let h_right ev l = abstract_tactic (TacLeft (ev,l)) (right_with_ebindings ev l)
+let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_ebindings ev l)
+(* Moved to tacinterp because of dependencies in Tacinterp.interp
 let h_any_constructor t =
   abstract_tactic (TacAnyConstructor t) (any_constructor t)
 *)
-let h_constructor n l =
-  abstract_tactic (TacConstructor(AI n,l))(constructor_tac None n l)
-let h_one_constructor n = h_constructor n NoBindings
-let h_simplest_left   = h_left NoBindings
-let h_simplest_right  = h_right NoBindings
+let h_constructor ev n l =
+  abstract_tactic (TacConstructor(ev,AI n,l))(constructor_tac ev None n l)
+let h_one_constructor n = h_constructor false n NoBindings
+let h_simplest_left   = h_left false NoBindings
+let h_simplest_right  = h_right false NoBindings
 
 (* Conversion *)
 let h_reduce r cl  = 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 84a5719374..8cbc28d1ec 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -80,10 +80,10 @@ val h_rename          : (identifier*identifier) list -> tactic
 val h_revert          : identifier list -> tactic
 
 (* Constructors *)
-val h_constructor     : int -> open_constr bindings -> tactic
-val h_left            : open_constr bindings -> tactic
-val h_right           : open_constr bindings -> tactic
-val h_split           : open_constr bindings -> tactic
+val h_constructor     : evars_flag -> int -> open_constr bindings -> tactic
+val h_left            : evars_flag -> open_constr bindings -> tactic
+val h_right           : evars_flag -> open_constr bindings -> tactic
+val h_split           : evars_flag -> open_constr bindings -> tactic
 
 val h_one_constructor : int -> tactic
 val h_simplest_left   : tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 55b8d08c6a..03eaf2d4d0 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -449,16 +449,15 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
 let raw_inversion inv_kind id status names gl =
   let env = pf_env gl and sigma = project gl in
   let c = mkVar id in
-  let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in
+  let (ind,t) = 
+    try pf_reduce_to_quantified_ind gl (pf_type_of gl c)
+    with UserError _ -> 
+      errorlabstrm "raw_inversion"
+	(str ("The type of "^(string_of_id id)^" is not inductive")) in
   let indclause = mk_clenv_from gl (c,t) in
-  let newc = clenv_value indclause in
   let ccl = clenv_type indclause in
   check_no_metas indclause ccl;
-  let IndType (indf,realargs) =
-    try find_rectype env sigma ccl
-    with Not_found ->
-      errorlabstrm "raw_inversion"
-	(str ("The type of "^(string_of_id id)^" is not inductive")) in
+  let IndType (indf,realargs) = find_rectype env sigma ccl in
   let (elim_predicate,neqns) =
     make_inv_predicate env sigma indf realargs id status (pf_concl gl) in
   let (cut_concl,case_tac) =
@@ -473,7 +472,7 @@ let raw_inversion inv_kind id status names gl =
      (true_cut Anonymous cut_concl)
      [case_tac names 
        (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
-       (Some elim_predicate) ([],[]) newc;
+       (Some elim_predicate) ([],[]) ind indclause;
       onLastHyp
         (fun id ->
            (tclTHEN
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 9f88213415..69840f85cd 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1712,7 +1712,7 @@ let check_evar_map_of_evars_defs evd =
   Evd.Metaset.iter
    (fun m ->
      if Evd.meta_defined evd m then () else
-      raise (Logic.RefinerError (Logic.OccurMetaGoal rebus)))
+      raise (Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m])))
  in
   List.iter
    (fun (_,binding) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9a2c2097c6..aba96afb3a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -215,10 +215,14 @@ let _ =
         "cofix", TacCofix None;
         "trivial", TacTrivial ([],None);
         "auto", TacAuto(None,[],None);
-        "left", TacLeft NoBindings;
-        "right", TacRight NoBindings;
-        "split", TacSplit(false,NoBindings);
-        "constructor", TacAnyConstructor None;
+        "left", TacLeft(false,NoBindings);
+        "eleft", TacLeft(true,NoBindings);
+        "right", TacRight(false,NoBindings);
+        "eright", TacRight(true,NoBindings);
+        "split", TacSplit(false,false,NoBindings);
+        "esplit", TacSplit(true,false,NoBindings);
+        "constructor", TacAnyConstructor (false,None);
+        "econstructor", TacAnyConstructor (true,None);
         "reflexivity", TacReflexivity;
         "symmetry", TacSymmetry nocl
       ];
@@ -721,11 +725,11 @@ let rec intern_atomic lf ist x =
   | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l)
 	
   (* Constructors *)
-  | TacLeft bl -> TacLeft (intern_bindings ist bl)
-  | TacRight bl -> TacRight (intern_bindings ist bl)
-  | TacSplit (b,bl) -> TacSplit (b,intern_bindings ist bl)
-  | TacAnyConstructor t -> TacAnyConstructor (Option.map (intern_tactic ist) t)
-  | TacConstructor (n,bl) -> TacConstructor (n, intern_bindings ist bl)
+  | TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl)
+  | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl)
+  | TacSplit (ev,b,bl) -> TacSplit (ev,b,intern_bindings ist bl)
+  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_tactic ist) t)
+  | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,intern_bindings ist bl)
 
   (* Conversion *)
   | TacReduce (r,cl) ->
@@ -2083,14 +2087,14 @@ and interp_atomic ist gl = function
   | TacRevert l -> h_revert (interp_hyp_list ist gl l)
 
   (* Constructors *)
-  | TacLeft bl -> h_left (interp_bindings ist gl bl)
-  | TacRight bl -> h_right (interp_bindings ist gl bl)
-  | TacSplit (_,bl) -> h_split (interp_bindings ist gl bl)
-  | TacAnyConstructor t ->
-      abstract_tactic (TacAnyConstructor t)
-        (Tactics.any_constructor (Option.map (interp_tactic ist) t))
-  | TacConstructor (n,bl) ->
-      h_constructor (skip_metaid n) (interp_bindings ist gl bl)
+  | TacLeft (ev,bl) -> h_left ev (interp_bindings ist gl bl)
+  | TacRight (ev,bl) -> h_right ev (interp_bindings ist gl bl)
+  | TacSplit (ev,_,bl) -> h_split ev (interp_bindings ist gl bl)
+  | TacAnyConstructor (ev,t) ->
+      abstract_tactic (TacAnyConstructor (ev,t))
+        (Tactics.any_constructor ev (Option.map (interp_tactic ist) t))
+  | TacConstructor (ev,n,bl) ->
+      h_constructor ev (skip_metaid n) (interp_bindings ist gl bl)
 
   (* Conversion *)
   | TacReduce (r,cl) ->
@@ -2391,11 +2395,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacRevert _ as x -> x
 
   (* Constructors *)
-  | TacLeft bl -> TacLeft (subst_bindings subst bl)
-  | TacRight bl -> TacRight (subst_bindings subst bl)
-  | TacSplit (b,bl) -> TacSplit (b,subst_bindings subst bl)
-  | TacAnyConstructor t -> TacAnyConstructor (Option.map (subst_tactic subst) t)
-  | TacConstructor (n,bl) -> TacConstructor (n, subst_bindings subst bl)
+  | TacLeft (ev,bl) -> TacLeft (ev,subst_bindings subst bl)
+  | TacRight (ev,bl) -> TacRight (ev,subst_bindings subst bl)
+  | TacSplit (ev,b,bl) -> TacSplit (ev,b,subst_bindings subst bl)
+  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (subst_tactic subst) t)
+  | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl)
 
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9bb6eef2c3..dd8aa12941 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -324,11 +324,11 @@ let last_arg c = match kind_of_term c with
   | App (f,cl) -> array_last cl
   | _ -> anomaly "last_arg"
 
-let general_elim_then_using 
-  elim isrec allnames tac predicate (indbindings,elimbindings) c gl =
-  let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+let general_elim_then_using mk_elim 
+  isrec allnames tac predicate (indbindings,elimbindings) 
+  ind indclause gl =
+  let elim = mk_elim ind gl in
   (* applying elimination_scheme just a little modified *)
-  let indclause  = mk_clenv_from gl (c,t) in
   let indclause' = clenv_match_args indbindings indclause in
   let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in
   let indmv = 
@@ -351,7 +351,7 @@ let general_elim_then_using
   in
   let elimclause' = clenv_fchain indmv elimclause indclause' in
   let elimclause' = clenv_match_args elimbindings elimclause' in
-  let branchsigns = compute_construtor_signatures isrec ity in
+  let branchsigns = compute_construtor_signatures isrec ind in
   let brnames = compute_induction_names (Array.length branchsigns) allnames in
   let after_tac ce i gl =
     let (hd,largs) = decompose_app ce.templtyp.Evd.rebus in
@@ -362,7 +362,7 @@ let general_elim_then_using
                    (fun acc b -> if b then acc+2 else acc+1)
                    0 branchsigns.(i);
                branchnum = i+1;
-               ity = ity;
+               ity = ind;
                largs = List.map (clenv_nf_meta ce) largs;
                pred = clenv_nf_meta ce hd }
     in 
@@ -377,37 +377,32 @@ let general_elim_then_using
   in 
   elim_res_pf_THEN_i elimclause' branchtacs gl
 
+(* computing the case/elim combinators *)
+
+let gl_make_elim ind gl =
+  Indrec.lookup_eliminator ind (elimination_sort_of_goal gl)
+
+let gl_make_case_dep ind gl =
+  pf_apply Indrec.make_case_dep gl ind (elimination_sort_of_goal gl)
+
+let gl_make_case_nodep ind gl =
+  pf_apply Indrec.make_case_nodep gl ind (elimination_sort_of_goal gl)
 
-let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
+let elimination_then_using tac predicate bindings c gl = 
   let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  let elim =
-    Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in
-  general_elim_then_using
-    elim true IntroAnonymous tac predicate (indbindings,elimbindings) c gl
+  let indclause  = mk_clenv_from gl (c,t) in
+  general_elim_then_using gl_make_elim
+    true IntroAnonymous tac predicate bindings ind indclause gl
+
+let case_then_using =
+  general_elim_then_using gl_make_case_dep false
 
+let case_nodep_then_using =
+  general_elim_then_using gl_make_case_nodep false
 
 let elimination_then tac        = elimination_then_using tac None 
 let simple_elimination_then tac = elimination_then tac ([],[])
 
-let case_then_using allnames tac predicate (indbindings,elimbindings) c gl =
-  (* finding the case combinator *)
-  let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  let sigma = project gl in 
-  let sort  = elimination_sort_of_goal gl  in
-  let elim  = Indrec.make_case_dep (pf_env gl) sigma ity sort in  
-  general_elim_then_using 
-    elim false allnames tac predicate (indbindings,elimbindings) c gl
-
-let case_nodep_then_using allnames tac predicate (indbindings,elimbindings)
-  c gl =
-  (* finding the case combinator *)
-  let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  let sigma = project gl in 
-  let sort  = elimination_sort_of_goal gl  in
-  let elim  = Indrec.make_case_nodep (pf_env gl) sigma ity sort in  
-  general_elim_then_using 
-    elim false allnames tac predicate (indbindings,elimbindings) c gl
-
 
 let make_elim_branch_assumptions ba gl =   
   let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc =
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index dd3b731351..d7620acf2d 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -138,9 +138,9 @@ val elimination_sort_of_goal : goal sigma -> sorts_family
 val elimination_sort_of_hyp  : identifier -> goal sigma -> sorts_family
 
 val general_elim_then_using :
-  constr -> (* isrec: *) bool -> intro_pattern_expr ->
+  (inductive -> goal sigma -> constr) -> rec_flag -> intro_pattern_expr ->
     (branch_args -> tactic) -> constr option -> 
-      (arg_bindings * arg_bindings) -> constr -> tactic
+      (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic
 	  
 val elimination_then_using :
   (branch_args -> tactic) -> constr option -> 
@@ -152,11 +152,13 @@ val elimination_then :
 
 val case_then_using :
   intro_pattern_expr -> (branch_args -> tactic) -> 
-    constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
+    constr option -> (arg_bindings * arg_bindings) ->
+      inductive -> clausenv -> tactic
 
 val case_nodep_then_using :
   intro_pattern_expr -> (branch_args -> tactic) -> 
-    constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
+    constr option -> (arg_bindings * arg_bindings) -> 
+      inductive -> clausenv -> tactic
 
 val simple_elimination_then :
   (branch_args -> tactic) -> constr -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 963025c3b2..b4e646a079 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -528,7 +528,7 @@ let error_uninstantiated_metas t clenv =
   in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id)
 
 let clenv_refine_in with_evars id clenv gl =
-  let clenv = if with_evars then clenv_pose_dependent_evars clenv else clenv in
+  let clenv = clenv_pose_dependent_evars with_evars clenv in
   let new_hyp_typ  = clenv_type clenv in
   if not with_evars & occur_meta new_hyp_typ then 
     error_uninstantiated_metas new_hyp_typ clenv;
@@ -672,9 +672,9 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 
 (* Resolution with missing arguments *)
 
-let apply_with_ebindings_gen advanced with_evars (c,lbind) gl =
+let general_apply with_delta with_destruct with_evars (c,lbind) gl =
   let flags = 
-    if advanced then default_unify_flags else default_no_delta_unify_flags in
+    if with_delta then default_unify_flags else default_no_delta_unify_flags in
   (* The actual type of the theorem. It will be matched against the
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
@@ -700,7 +700,8 @@ let apply_with_ebindings_gen advanced with_evars (c,lbind) gl =
 	   second order unification *)
 	try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit
 	with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
-	  if advanced then
+	  if with_destruct then
+	   try
 	    let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
 	    match match_with_conjunction (snd (decompose_prod t)) with
 	    | Some _ ->
@@ -717,14 +718,15 @@ let apply_with_ebindings_gen advanced with_evars (c,lbind) gl =
 			tclTHEN (try_main_apply (mkVar id)) (thin l)) l))
 		]) gl
 	    | None ->
-	      raise exn
+		raise Exit
+	   with RefinerError _|UserError _|Exit -> raise exn 
 	  else
-	    raise exn in
+	    raise exn
+ in
     try_red_apply thm_ty0 in
   try_main_apply c gl
 
-let advanced_apply_with_ebindings = apply_with_ebindings_gen true false
-let advanced_eapply_with_ebindings = apply_with_ebindings_gen true true
+let apply_with_ebindings_gen b = general_apply b b
 
 let apply_with_ebindings = apply_with_ebindings_gen false false
 let eapply_with_ebindings = apply_with_ebindings_gen false true
@@ -942,45 +944,47 @@ let check_number_of_constructors expctdnumopt i nconstr =
   end;
   if i > nconstr then error "Not enough constructors"
 
-let constructor_tac expctdnumopt i lbind gl =
+let constructor_tac with_evars expctdnumopt i lbind gl =
   let cl = pf_concl gl in 
   let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in 
   let nconstr =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
   check_number_of_constructors expctdnumopt i nconstr;
   let cons = mkConstruct (ith_constructor_of_inductive mind i) in
-  let apply_tac = advanced_apply_with_ebindings (cons,lbind) in
+  let apply_tac = general_apply true false with_evars (cons,lbind) in
   (tclTHENLIST 
      [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
 
-let one_constructor i = constructor_tac None i
+let one_constructor i = constructor_tac false None i
 
 (* Try to apply the constructor of the inductive definition followed by 
    a tactic t given as an argument.
    Should be generalize in Constructor (Fun c : I -> tactic)
  *)
 
-let any_constructor tacopt gl =
+let any_constructor with_evars tacopt gl =
   let t = match tacopt with None -> tclIDTAC | Some t -> t in
   let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in
   let nconstr =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
   if nconstr = 0 then error "The type has no constructors";
-  tclFIRST (List.map (fun i -> tclTHEN (one_constructor i NoBindings) t) 
-              (interval 1 nconstr)) gl
+  tclFIRST
+    (List.map
+      (fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t) 
+      (interval 1 nconstr)) gl
 
-let left_with_ebindings  = constructor_tac (Some 2) 1
-let right_with_ebindings = constructor_tac (Some 2) 2
-let split_with_ebindings = constructor_tac (Some 1) 1
+let left_with_ebindings  with_evars = constructor_tac with_evars (Some 2) 1
+let right_with_ebindings with_evars = constructor_tac with_evars (Some 2) 2
+let split_with_ebindings with_evars = constructor_tac with_evars (Some 1) 1
 
-let left l         = left_with_ebindings (inj_ebindings l)
-let simplest_left  = left NoBindings
+let left l             = left_with_ebindings false (inj_ebindings l)
+let simplest_left      = left NoBindings
 
-let right l        = right_with_ebindings (inj_ebindings l)
-let simplest_right = right NoBindings
+let right l            = right_with_ebindings false (inj_ebindings l)
+let simplest_right     = right NoBindings
 
-let split l        = split_with_ebindings (inj_ebindings l)
-let simplest_split = split NoBindings
+let split l            = split_with_ebindings false (inj_ebindings l)
+let simplest_split     = split NoBindings
 
 
 (*****************************)
@@ -1742,13 +1746,14 @@ let make_base n id =
 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 ind_prefix = "IH" 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
+	| None -> id_of_string ind_prefix
+	| Some ind_id -> add_prefix ind_prefix (Nametab.id_of_global ind_id)
+    else add_prefix ind_prefix cname in
+  let hyprecname = make_base n base_ind in
   let avoid =
     if n=1 (* Only one recursive argument *) or n=0 then []
     else
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 1c64e47e84..1b2b7b38fa 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -182,9 +182,6 @@ val eapply_with_bindings  : constr with_bindings -> tactic
 val apply_with_ebindings  : constr with_ebindings -> tactic
 val eapply_with_ebindings : constr with_ebindings -> tactic
 
-val advanced_apply_with_ebindings  : constr with_ebindings -> tactic
-val advanced_eapply_with_ebindings : constr with_ebindings -> tactic
-
 val cut_and_apply         : constr -> tactic
 
 val apply_in : evars_flag -> identifier -> constr with_ebindings list -> tactic
@@ -282,22 +279,22 @@ val dorE : bool -> clause ->tactic
 
 (*s Introduction tactics. *)
 
-val constructor_tac            : int option -> int -> 
-                                 open_constr bindings  -> tactic
-val one_constructor            : int -> open_constr bindings  -> tactic
-val any_constructor            : tactic option -> tactic
+val constructor_tac      : evars_flag -> int option -> int -> 
+                           open_constr bindings  -> tactic
+val any_constructor      : evars_flag -> tactic option -> tactic
+val one_constructor      : int -> open_constr bindings  -> tactic
 
-val left                       : constr bindings -> tactic
-val right                      : constr bindings -> tactic
-val split                      : constr bindings -> tactic
+val left                 : constr bindings -> tactic
+val right                : constr bindings -> tactic
+val split                : constr bindings -> tactic
 
-val left_with_ebindings        : open_constr bindings -> tactic
-val right_with_ebindings       : open_constr bindings -> tactic
-val split_with_ebindings       : open_constr bindings -> tactic
+val left_with_ebindings  : evars_flag -> open_constr bindings -> tactic
+val right_with_ebindings : evars_flag -> open_constr bindings -> tactic
+val split_with_ebindings : evars_flag -> open_constr bindings -> tactic
 
-val simplest_left              : tactic
-val simplest_right             : tactic
-val simplest_split             : tactic
+val simplest_left        : tactic
+val simplest_right       : tactic
+val simplest_split       : tactic
 
 (*s Logical connective tactics. *)