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

9 files changed, 125 insertions, 115 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 62ed700a27..535fd6632e 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -77,7 +77,7 @@ let contradiction_term (c,lbind as cl) gl =
   let typ = pf_type_of gl c in
   let _, ccl = splay_prod env sigma typ in
   if is_empty_type ccl then
-    tclTHEN (elim cl None) (tclTRY assumption) gl
+    tclTHEN (elim false cl None) (tclTRY assumption) gl
   else
     try
       if lbind = NoBindings then
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 60cedf093c..134f018caf 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -762,7 +762,7 @@ let rec consider_match may_intro introduced available expected gls =
 		 try conjunction_arity id gls with 
 		     Not_found -> error "matching hypothesis not found" in 
 		 tclTHENLIST 
-		   [general_case_analysis (mkVar id,NoBindings);
+		   [general_case_analysis false (mkVar id,NoBindings);
 		    intron_then nhyps []
 		      (fun l -> consider_match may_intro introduced 
 			 (List.rev_append l rest_ids) expected)] gls)
@@ -1347,7 +1347,7 @@ let end_tac et2 gls =
 	      tclSOLVE [simplest_elim pi.per_casee]	
 	  | ET_Case_analysis,EK_nodep ->
 	      tclTHEN 
-		(general_case_analysis (pi.per_casee,NoBindings))
+		(general_case_analysis false (pi.per_casee,NoBindings))
 		(default_justification (List.map mkVar clauses))
 	  | ET_Induction,EK_nodep ->
 	      tclTHENLIST
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7681a03a4e..066bf88d44 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -61,7 +61,7 @@ let general_elim_clause with_evars cls c elim = match cls with
       (* was tclWEAK_PROGRESS which only fails for tactics generating one 
          subgoal and did not fail for useless conditional rewritings generating
          an extra condition *)
-      tclNOTSAMEGOAL (general_elim c elim ~allow_K:false)
+      tclNOTSAMEGOAL (general_elim with_evars c elim ~allow_K:false)
   | Some id ->
       general_elim_in with_evars id c elim 
 
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 55666a08a6..8bb7c5c2ce 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -23,7 +23,7 @@ let inj_id id = (dummy_loc,id)
 let inj_open c = (Evd.empty,c)
 let inj_open_wb (c,b) = ((Evd.empty,c),b)
 let inj_ia = function
-  | ElimOnConstr c -> ElimOnConstr (inj_open c)
+  | ElimOnConstr c -> ElimOnConstr (inj_open_wb c)
   | ElimOnIdent id -> ElimOnIdent id
   | ElimOnAnonHyp n -> ElimOnAnonHyp n
 let inj_occ (occ,c) = (occ,inj_open c)
@@ -42,11 +42,11 @@ let h_vm_cast_no_check c =
 let h_apply ev cb    =
   abstract_tactic (TacApply (ev,inj_open_wb cb))
     (apply_with_ebindings_gen ev cb)
-let h_elim cb cbo    =
-  abstract_tactic (TacElim (inj_open_wb cb,option_map inj_open_wb cbo))
-    (elim cb cbo)
+let h_elim ev cb cbo    =
+  abstract_tactic (TacElim (ev,inj_open_wb cb,option_map inj_open_wb cbo))
+    (elim ev cb cbo)
 let h_elim_type c    = abstract_tactic (TacElimType (inj_open c)) (elim_type c)
-let h_case cb        = abstract_tactic (TacCase (inj_open_wb cb)) (general_case_analysis cb)
+let h_case ev cb     = abstract_tactic (TacCase (ev,inj_open_wb cb)) (general_case_analysis ev cb)
 let h_case_type c    = abstract_tactic (TacCaseType (inj_open c)) (case_type c)
 let h_fix ido n      = abstract_tactic (TacFix (ido,n)) (fix ido n)
 let h_mutual_fix id n l =
@@ -77,12 +77,12 @@ let h_simple_induction h =
   abstract_tactic (TacSimpleInduction h) (simple_induct h)
 let h_simple_destruct h  =
   abstract_tactic (TacSimpleDestruct h) (simple_destruct h)
-let h_new_induction c e idl =
-  abstract_tactic (TacNewInduction (List.map inj_ia c,option_map inj_open_wb e,idl))
-    (new_induct c e idl)
-let h_new_destruct c e idl =
-  abstract_tactic (TacNewDestruct (List.map inj_ia c,option_map inj_open_wb e,idl))
-    (new_destruct c e idl)
+let h_new_induction ev c e idl =
+  abstract_tactic (TacNewInduction (ev,List.map inj_ia c,option_map inj_open_wb e,idl))
+    (new_induct ev c e idl)
+let h_new_destruct ev c e idl =
+  abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,option_map inj_open_wb e,idl))
+    (new_destruct ev c e idl)
 let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (new_hyp n d)
 let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c)
 
@@ -124,8 +124,8 @@ let h_transitivity c =
 
 let h_simplest_apply c  = h_apply false (c,NoBindings)
 let h_simplest_eapply c = h_apply true (c,NoBindings)
-let h_simplest_elim c   = h_elim (c,NoBindings) None
-let h_simplest_case   c = h_case (c,NoBindings)
+let h_simplest_elim c   = h_elim false (c,NoBindings) None
+let h_simplest_case   c = h_case false (c,NoBindings)
 
 let h_intro_patterns l = abstract_tactic (TacIntroPattern l) (intro_patterns l)
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 8937a37ef0..87232988b8 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -17,6 +17,7 @@ open Genarg
 open Tacexpr
 open Rawterm
 open Evd
+open Clenv
 (*i*)
 
 (* Tactics for the interpreter. They left a trace in the proof tree
@@ -35,10 +36,10 @@ val h_vm_cast_no_check  : constr -> tactic
 
 val h_apply           : evars_flag -> constr with_ebindings -> tactic
 
-val h_elim            : constr with_ebindings ->
+val h_elim            : evars_flag -> constr with_ebindings ->
                         constr with_ebindings option -> tactic
 val h_elim_type       : constr -> tactic
-val h_case            : constr with_ebindings -> tactic
+val h_case            : evars_flag -> constr with_ebindings -> tactic
 val h_case_type       : constr -> tactic
 
 val h_mutual_fix      : identifier -> int ->
@@ -59,11 +60,11 @@ val h_instantiate     : int -> Rawterm.rawconstr ->
 val h_simple_induction   : quantified_hypothesis -> tactic
 val h_simple_destruct    : quantified_hypothesis -> tactic
 val h_new_induction   :
-  constr induction_arg list -> constr with_ebindings option ->
-  intro_pattern_expr -> tactic
+  evars_flag -> constr with_ebindings induction_arg list ->
+    constr with_ebindings option -> intro_pattern_expr -> tactic
 val h_new_destruct    :
-  constr induction_arg list -> constr with_ebindings option -> 
-  intro_pattern_expr -> tactic
+  evars_flag -> constr with_ebindings induction_arg list ->
+    constr with_ebindings option -> intro_pattern_expr -> tactic
 val h_specialize      : int option -> constr with_ebindings -> tactic
 val h_lapply          : constr -> tactic
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index daa6e27779..bfaa7e5e48 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -111,7 +111,8 @@ let make_inv_predicate env sigma indf realargs id status concl =
               | None ->
 		let sort = get_sort_of env sigma concl in
 		let p = make_arity env true indf sort in
-		Unification.abstract_list_all env sigma p concl (realargs@[mkVar id]) in
+		Unification.abstract_list_all env (Evd.create_evar_defs sigma)
+		  p concl (realargs@[mkVar id]) in
 	  let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in
 	  (* We lift to make room for the equations *)
 	  (hyps,lift nrealargs bodypred)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1a6c18e4dd..bff8b1b49b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -492,12 +492,12 @@ let intern_clause_pattern ist (l,occl) =
 
   (* TODO: catch ltac vars *)
 let intern_induction_arg ist = function
-  | ElimOnConstr c -> ElimOnConstr (intern_constr ist c)
+  | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c)
   | ElimOnAnonHyp n as x -> x
   | ElimOnIdent (loc,id) ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-	ElimOnConstr (intern_constr ist (CRef (Ident (dloc,id))))
+	ElimOnConstr (intern_constr ist (CRef (Ident (dloc,id))),NoBindings)
       else
 	ElimOnIdent (loc,id)
 
@@ -660,11 +660,11 @@ let rec intern_atomic lf ist x =
   | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
   | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
   | TacApply (ev,cb) -> TacApply (ev,intern_constr_with_bindings ist cb)
-  | TacElim (cb,cbo) ->
-      TacElim (intern_constr_with_bindings ist cb,
+  | TacElim (ev,cb,cbo) ->
+      TacElim (ev,intern_constr_with_bindings ist cb,
                option_map (intern_constr_with_bindings ist) cbo)
   | TacElimType c -> TacElimType (intern_type ist c)
-  | TacCase cb -> TacCase (intern_constr_with_bindings ist cb)
+  | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
   | TacCaseType c -> TacCaseType (intern_type ist c)
   | TacFix (idopt,n) -> TacFix (option_map (intern_ident lf ist) idopt,n)
   | TacMutualFix (id,n,l) ->
@@ -702,14 +702,14 @@ let rec intern_atomic lf ist x =
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
       TacSimpleInduction (intern_quantified_hypothesis ist h)
-  | TacNewInduction (lc,cbo,ids) ->
-      TacNewInduction (List.map (intern_induction_arg ist) lc,
+  | TacNewInduction (ev,lc,cbo,ids) ->
+      TacNewInduction (ev,List.map (intern_induction_arg ist) lc,
                option_map (intern_constr_with_bindings ist) cbo,
                (intern_intro_pattern lf ist ids))
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
-  | TacNewDestruct (c,cbo,ids) ->
-      TacNewDestruct (List.map (intern_induction_arg ist) c,
+  | TacNewDestruct (ev,c,cbo,ids) ->
+      TacNewDestruct (ev,List.map (intern_induction_arg ist) c,
                option_map (intern_constr_with_bindings ist) cbo,
 	       (intern_intro_pattern lf ist ids))
   | TacDoubleInduction (h1,h2) ->
@@ -1558,14 +1558,6 @@ let interp_declared_or_quantified_hypothesis ist gl = function
 	    (coerce_to_decl_or_quant_hyp env) ist (Some env) (dloc,id)
       with Not_found -> NamedHyp id
 
-let interp_induction_arg ist gl = function
-  | ElimOnConstr c -> ElimOnConstr (pf_interp_constr ist gl c)
-  | ElimOnAnonHyp n as x -> x
-  | ElimOnIdent (loc,id) ->
-      if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
-      else ElimOnConstr
-	(pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))))
-
 let interp_binding ist gl (loc,b,c) =
   (loc,interp_binding_name ist b,pf_interp_open_constr false ist gl c)
 
@@ -1580,6 +1572,15 @@ let interp_constr_with_bindings ist gl (c,bl) =
 let interp_open_constr_with_bindings ist gl (c,bl) =
   (pf_interp_open_constr false ist gl c, interp_bindings ist gl bl)
 
+let interp_induction_arg ist gl = function
+  | ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c)
+  | ElimOnAnonHyp n as x -> x
+  | ElimOnIdent (loc,id) ->
+      if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
+      else ElimOnConstr
+	(pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))),
+	 NoBindings)
+
 let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c)
 let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c))
 let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
@@ -2085,11 +2086,11 @@ and interp_atomic ist gl = function
   | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
   | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c)
   | TacApply (ev,cb) -> h_apply ev (interp_constr_with_bindings ist gl cb)
-  | TacElim (cb,cbo) ->
-      h_elim (interp_constr_with_bindings ist gl cb)
+  | TacElim (ev,cb,cbo) ->
+      h_elim ev (interp_constr_with_bindings ist gl cb)
                 (option_map (interp_constr_with_bindings ist gl) cbo)
   | TacElimType c -> h_elim_type (pf_interp_type ist gl c)
-  | TacCase cb -> h_case (interp_constr_with_bindings ist gl cb)
+  | TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb)
   | TacCaseType c -> h_case_type (pf_interp_type ist gl c)
   | TacFix (idopt,n) -> h_fix (option_map (interp_fresh_ident ist gl) idopt) n
   | TacMutualFix (id,n,l) ->
@@ -2130,14 +2131,14 @@ and interp_atomic ist gl = function
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
       h_simple_induction (interp_quantified_hypothesis ist h)
-  | TacNewInduction (lc,cbo,ids) ->
-      h_new_induction (List.map (interp_induction_arg ist gl) lc)
+  | TacNewInduction (ev,lc,cbo,ids) ->
+      h_new_induction ev (List.map (interp_induction_arg ist gl) lc)
         (option_map (interp_constr_with_bindings ist gl) cbo)
         (interp_intro_pattern ist gl ids)
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist h)
-  | TacNewDestruct (c,cbo,ids) -> 
-      h_new_destruct (List.map (interp_induction_arg ist gl) c)
+  | TacNewDestruct (ev,c,cbo,ids) -> 
+      h_new_destruct ev (List.map (interp_induction_arg ist gl) c)
         (option_map (interp_constr_with_bindings ist gl) cbo)
         (interp_intro_pattern ist gl ids)
   | TacDoubleInduction (h1,h2) ->
@@ -2337,7 +2338,7 @@ let subst_raw_with_bindings subst (c,bl) =
   (subst_rawconstr subst c, subst_bindings subst bl)
 
 let subst_induction_arg subst = function
-  | ElimOnConstr c -> ElimOnConstr (subst_rawconstr subst c)
+  | ElimOnConstr c -> ElimOnConstr (subst_raw_with_bindings subst c)
   | ElimOnAnonHyp n as x -> x
   | ElimOnIdent id as x -> x
 
@@ -2413,11 +2414,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c)
   | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c)
   | TacApply (ev,cb) -> TacApply (ev,subst_raw_with_bindings subst cb)
-  | TacElim (cb,cbo) ->
-      TacElim (subst_raw_with_bindings subst cb,
+  | TacElim (ev,cb,cbo) ->
+      TacElim (ev,subst_raw_with_bindings subst cb,
                option_map (subst_raw_with_bindings subst) cbo)
   | TacElimType c -> TacElimType (subst_rawconstr subst c)
-  | TacCase cb -> TacCase (subst_raw_with_bindings subst cb)
+  | TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb)
   | TacCaseType c -> TacCaseType (subst_rawconstr subst c)
   | TacFix (idopt,n) as x -> x
   | TacMutualFix (id,n,l) ->
@@ -2443,12 +2444,12 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 
   (* Derived basic tactics *)
   | TacSimpleInduction h as x -> x
-  | TacNewInduction (lc,cbo,ids) -> (* Pierre C. est-ce correct? *)
-      TacNewInduction (List.map (subst_induction_arg subst) lc,
+  | TacNewInduction (ev,lc,cbo,ids) ->
+      TacNewInduction (ev,List.map (subst_induction_arg subst) lc,
                option_map (subst_raw_with_bindings subst) cbo, ids)
   | TacSimpleDestruct h as x -> x
-  | TacNewDestruct (c,cbo,ids) ->
-      TacNewDestruct (List.map (subst_induction_arg subst) c,  (* Julien F. est-ce correct? *)
+  | TacNewDestruct (ev,c,cbo,ids) ->
+      TacNewDestruct (ev,List.map (subst_induction_arg subst) c,
                option_map (subst_raw_with_bindings subst) cbo, ids)
   | TacDoubleInduction (h1,h2) as x -> x
   | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 65610fe279..cffe550afc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -554,8 +554,7 @@ let apply_with_ebindings_gen with_evars (c,lbind) gl =
     let n = nb_prod thm_ty - nprod in
     if n<0 then error "Apply: theorem has not enough premisses.";
     let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
-    if with_evars then Clenvtac.e_res_pf clause gl
-    else Clenvtac.res_pf clause gl in
+    Clenvtac.res_pf clause ~with_evars:with_evars gl in
   try try_apply thm_ty0 concl_nprod
   with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->
     let rec try_red_apply thm_ty =
@@ -824,7 +823,7 @@ let last_arg c = match kind_of_term c with
       array_last cl
   | _ -> anomaly "last_arg"
 	
-let elimination_clause_scheme allow_K elimclause indclause gl = 
+let elimination_clause_scheme with_evars allow_K elimclause indclause gl = 
   let indmv = 
     (match kind_of_term (last_arg elimclause.templval.rebus) with
        | Meta mv -> mv
@@ -832,7 +831,7 @@ let elimination_clause_scheme allow_K elimclause indclause gl =
              (str "The type of elimination clause is not well-formed")) 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause in 
-  res_pf elimclause' ~allow_K:allow_K gl
+  res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K gl
 
 (* cast added otherwise tactics Case (n1,n2) generates (?f x y) and 
  * refine fails *)
@@ -856,8 +855,8 @@ let general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl =
   let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in 
     elimtac elimclause indclause gl
 
-let general_elim c e ?(allow_K=true) =
-  general_elim_clause (elimination_clause_scheme allow_K) c e
+let general_elim with_evars c e ?(allow_K=true) =
+  general_elim_clause (elimination_clause_scheme with_evars allow_K) c e
 
 (* Elimination tactic with bindings but using the default elimination 
  * constant associated with the type. *)
@@ -866,22 +865,23 @@ let find_eliminator c gl =
   let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   lookup_eliminator ind (elimination_sort_of_goal gl)
 
-let default_elim (c,_ as cx) gl = 
-  general_elim cx (find_eliminator c gl,NoBindings) gl
+let default_elim with_evars (c,_ as cx) gl = 
+  general_elim with_evars cx (find_eliminator c gl,NoBindings) gl
 
-let elim_in_context c = function
-  | Some elim -> general_elim c elim ~allow_K:true
-  | None -> default_elim c
+let elim_in_context with_evars c = function
+  | Some elim -> general_elim with_evars c elim ~allow_K:true
+  | None -> default_elim with_evars c
 
-let elim (c,lbindc as cx) elim =
+let elim with_evars (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
+	tclTHEN (tclTRY (intros_until_id id))
+	  (elim_in_context with_evars cx elim)
+    | _ -> elim_in_context with_evars cx elim
 
 (* The simplest elimination tactic, with no substitutions at all. *)
 
-let simplest_elim c = default_elim (c,NoBindings)
+let simplest_elim c = default_elim false (c,NoBindings)
 
 (* Elimination in hypothesis *)
 (* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y)
@@ -915,23 +915,23 @@ let general_elim_in with_evars id =
 
 (* Case analysis tactics *)
 
-let general_case_analysis_in_context (c,lbindc) gl =
+let general_case_analysis_in_context with_evars (c,lbindc) gl =
   let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   let sort     = elimination_sort_of_goal gl in
   let case = 
     if occur_term c (pf_concl gl) then make_case_dep else make_case_gen in
   let elim     = pf_apply case gl mind sort in 
-  general_elim (c,lbindc) (elim,NoBindings) gl
+  general_elim with_evars (c,lbindc) (elim,NoBindings) gl
 
-let general_case_analysis (c,lbindc as cx) =
+let general_case_analysis with_evars (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 with_evars cx)
     | _ ->
-	general_case_analysis_in_context cx
+	general_case_analysis_in_context with_evars cx
 
-let simplest_case c = general_case_analysis (c,NoBindings)
+let simplest_case c = general_case_analysis false (c,NoBindings)
 
 (*****************************)
 (* Decomposing introductions *)
@@ -1615,16 +1615,15 @@ let empty_scheme =
 
 (* Unification between ((elimc:elimt) ?i ?j ?k ?l ... ?m) and the
    hypothesis on which the induction is made *)
-let induction_tac varname typ scheme (*(elimc,lbindelimc),elimt*) gl =
+let induction_tac with_evars (varname,lbind) typ scheme gl =
   let elimc,lbindelimc = 
     match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in
   let elimt = scheme.elimt in
-  let c = mkVar varname in
-  let indclause  = make_clenv_binding gl (c,typ) NoBindings  in
+  let indclause = make_clenv_binding gl (mkVar varname,typ) lbind  in
   let elimclause =
     make_clenv_binding gl 
       (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
-  elimination_clause_scheme true elimclause indclause gl
+  elimination_clause_scheme with_evars true elimclause indclause gl
 
 let make_base n id =
   if n=0 or n=1 then id
@@ -2134,7 +2133,7 @@ let recolle_clenv scheme lid elimclause gl =
    (elimc ?i ?j ?k...?l). This solves partly meta variables (and may
     produce new ones). Then refine with the resulting term with holes.
 *)
-let induction_tac_felim indvars (* (elimc,lbindelimc) elimt *) scheme gl = 
+let induction_tac_felim with_evars indvars (* (elimc,lbindelimc) elimt *) scheme gl = 
   let elimt = scheme.elimt in
   let elimc,lbindelimc = 
     match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in
@@ -2145,7 +2144,7 @@ let induction_tac_felim indvars (* (elimc,lbindelimc) elimt *) scheme gl =
   let elimclause' = recolle_clenv scheme indvars elimclause gl in
   (* one last resolution (useless?) *)
   let resolved = clenv_unique_resolver true elimclause' gl in
-  clenv_refine resolved gl
+  clenv_refine with_evars resolved gl
 
 (* Induction with several induction arguments, main differences with
    induction_from_context is that there is no main induction argument,
@@ -2153,7 +2152,7 @@ let induction_tac_felim indvars (* (elimc,lbindelimc) elimt *) scheme gl =
    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_l isrec elim_info lid names gl =
+let induction_from_context_l isrec with_evars elim_info lid names gl =
   let indsign,scheme = elim_info in
   (* number of all args, counting farg and indarg if present. *)
   let nargs_indarg_farg = scheme.nargs
@@ -2202,7 +2201,7 @@ let induction_from_context_l isrec elim_info lid names gl =
 	  (* Induction by "refine (indscheme ?i ?j ?k...)" + resolution of all
 	     possible holes using arguments given by the user (but the
 	     functional one). *)
-	  induction_tac_felim realindvars scheme;
+	  induction_tac_felim with_evars realindvars scheme;
           tclTRY (thin (List.rev (indhyps)));
 	])
 	(array_map2 
@@ -2212,7 +2211,7 @@ let induction_from_context_l isrec elim_info lid names gl =
 
 
 
-let induction_from_context isrec elim_info hyp0 names gl =
+let induction_from_context isrec with_evars elim_info (hyp0,lbind) names 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" 
@@ -2247,7 +2246,7 @@ let induction_from_context isrec elim_info hyp0 names gl =
       thin dephyps;
       (if isrec then tclTHENFIRSTn else tclTHENLASTn)
        	(tclTHENLIST
-	  [ induction_tac hyp0 typ0 scheme (*scheme.elimc,scheme.elimt*);
+	  [ induction_tac with_evars (hyp0,lbind) typ0 scheme;
 	    tclTHEN (tclTRY (unfold_body hyp0)) (thin [hyp0]);
             tclTRY (thin indhyps) ])
        	(array_map2
@@ -2259,22 +2258,22 @@ let induction_from_context isrec elim_info hyp0 names gl =
 
 exception TryNewInduct of exn
 
-let induction_with_atomization_of_ind_arg isrec elim names hyp0 gl =
+let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) gl =
   let (indsign,scheme as elim_info) = find_elim_signature isrec elim hyp0 gl in
   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_l isrec elim_info [hyp0] names gl
+    induction_from_context_l isrec with_evars elim_info [hyp0] names gl
   else
     let indref = match scheme.indref with | None -> assert false | Some x -> x in
     tclTHEN
       (atomize_param_of_ind (indref,scheme.nparams) hyp0)
-      (induction_from_context isrec elim_info hyp0 names) gl
+      (induction_from_context isrec with_evars elim_info (hyp0,lbind) names) gl
 
 (* Induction on a list of induction arguments. Analyse the elim
    scheme (which is mandatory for multiple ind args), check that all
    parameters and arguments are given (mandatory too). *)
-let induction_without_atomization isrec elim names lid gl =
+let induction_without_atomization isrec with_evars elim names lid gl =
   let (indsign,scheme as elim_info) =
     find_elim_signature isrec elim (List.hd lid) gl in
   let awaited_nargs = 
@@ -2285,26 +2284,29 @@ 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_l isrec elim_info lid names gl
+  else induction_from_context_l isrec with_evars elim_info lid names gl
 
-let new_induct_gen isrec elim names c gl =
+let new_induct_gen isrec with_evars elim names (c,lbind) gl =
   match kind_of_term c with
-    | Var id when not (mem_named_context id (Global.named_context())) ->
-	induction_with_atomization_of_ind_arg isrec elim names id gl
+    | Var id when not (mem_named_context id (Global.named_context()))
+	        & lbind = NoBindings & not with_evars ->
+	induction_with_atomization_of_ind_arg
+	  isrec with_evars elim names (id,lbind) gl
     | _        ->
 	let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) 
 		  Anonymous in
 	let id = fresh_id [] x gl in
 	tclTHEN
 	  (letin_tac true (Name id) c allClauses)
-	  (induction_with_atomization_of_ind_arg isrec elim names id) gl
+	  (induction_with_atomization_of_ind_arg
+	     isrec with_evars elim names (id,lbind)) gl
 
 (* Induction on a list of arguments. First make induction arguments
    atomic (using letins), then do induction. The specificity here is
    that all arguments and parameters of the scheme are given
    (mandatory for the moment), so we don't need to deal with
     parameters of the inductive type as in new_induct_gen. *)
-let new_induct_gen_l isrec elim names lc gl =
+let new_induct_gen_l isrec with_evars elim names lc gl =
   let newlc = ref [] in
   let letids = ref [] in
   let rec atomize_list l gl =
@@ -2331,7 +2333,7 @@ let new_induct_gen_l isrec elim names lc gl =
     [
       (atomize_list lc);
       (fun gl' -> (* recompute each time to have the new value of newlc *)
-	induction_without_atomization isrec elim names !newlc gl') ;
+	induction_without_atomization isrec with_evars elim names !newlc gl') ;
       (* after induction, try to unfold all letins created by atomize_list
          FIXME: unfold_all does not exist anywhere else? *)
       (fun gl' -> (* recompute each time to have the new value of letids *)
@@ -2340,7 +2342,7 @@ let new_induct_gen_l isrec elim names lc gl =
     gl
 
 
-let induct_destruct_l isrec lc elim names = 
+let induct_destruct_l isrec with_evars lc elim names = 
   (* Several induction hyps: induction scheme is mandatory *)
   let _ = 
     if elim = None 
@@ -2351,10 +2353,10 @@ let induct_destruct_l isrec lc elim names =
     List.map
       (fun x -> 
 	match x with (* FIXME: should we deal with ElimOnIdent? *)
-	  | ElimOnConstr x -> x
+	  | ElimOnConstr (x,NoBindings) -> x
 	  | _ -> error "don't know where to find some argument")
       lc in
-  new_induct_gen_l isrec elim names newlc
+  new_induct_gen_l isrec with_evars elim names newlc
 
 
 (* Induction either over a term, over a quantified premisse, or over
@@ -2362,24 +2364,27 @@ let induct_destruct_l isrec lc elim names =
    principles). 
    TODO: really unify induction with one and induction with several
    args *)
-let induct_destruct isrec lc elim names = 
+let induct_destruct isrec with_evars lc elim names = 
   assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
   if List.length lc = 1 then (* induction on one arg: use old mechanism *)
     try 
       let c = List.hd lc in
       match c with
-	| ElimOnConstr c -> new_induct_gen isrec elim names c
+	| ElimOnConstr c -> new_induct_gen isrec with_evars elim names c
 	| ElimOnAnonHyp n ->
 	    tclTHEN (intros_until_n n)
-	      (tclLAST_HYP (new_induct_gen isrec elim names))
+	      (tclLAST_HYP (fun c -> 
+		  new_induct_gen isrec with_evars elim names (c,NoBindings)))
 	      (* Identifier apart because id can be quantified in goal and not typable *)
 	| ElimOnIdent (_,id) ->
 	    tclTHEN (tclTRY (intros_until_id id))
-	      (new_induct_gen isrec elim names (mkVar id))
+	      (new_induct_gen isrec with_evars elim names (mkVar id,NoBindings))
     with (* If this fails, try with new mechanism but if it fails too,
 	    then the exception is the first one. *)
-      | x -> (try induct_destruct_l isrec lc elim names with _  -> raise x)
-  else induct_destruct_l isrec lc elim names
+      | x ->
+	  (try induct_destruct_l isrec with_evars lc elim names
+	   with _  -> raise x)
+  else induct_destruct_l isrec with_evars lc elim names
 
 
       
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index dfadeb54f6..eb62f602aa 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -231,27 +231,29 @@ type elim_scheme = {
 
 val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme
 
-val general_elim  :
+val general_elim  : evars_flag ->
   constr with_ebindings -> constr with_ebindings -> ?allow_K:bool -> tactic
 val general_elim_in : evars_flag -> 
   identifier -> constr with_ebindings -> constr with_ebindings -> tactic
 
-val default_elim  : constr with_ebindings -> tactic
+val default_elim  : evars_flag -> constr with_ebindings -> tactic
 val simplest_elim : constr -> tactic
-val elim          : constr with_ebindings -> constr with_ebindings option -> tactic
+val elim : 
+  evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic
+
 val simple_induct : quantified_hypothesis -> tactic
 
-val new_induct : constr induction_arg list -> constr with_ebindings option ->
-  intro_pattern_expr -> tactic
+val new_induct : evars_flag -> constr with_ebindings induction_arg list -> 
+  constr with_ebindings option -> intro_pattern_expr -> tactic
 
 (*s Case analysis tactics. *)
 
-val general_case_analysis : constr with_ebindings ->  tactic
+val general_case_analysis : evars_flag -> constr with_ebindings ->  tactic
 val simplest_case         : constr -> tactic
 
 val simple_destruct          : quantified_hypothesis -> tactic
-val new_destruct : constr induction_arg list -> constr with_ebindings option ->
-  intro_pattern_expr -> tactic
+val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> 
+  constr with_ebindings option -> intro_pattern_expr -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)