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

3 files changed, 19 insertions, 18 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 785316d56..ad19bd9b6 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -60,25 +60,22 @@ let clenv_cast_meta clenv =
   in 
   crec
 
-let clenv_refine clenv gls =
+let clenv_refine with_evars clenv gls =
+  let clenv = if with_evars then clenv_pose_dependent_evars clenv else clenv in
   tclTHEN
     (tclEVARS (evars_of clenv.evd)) 
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
     gls
 
 
-let res_pf clenv ?(allow_K=false) gls =
-  clenv_refine (clenv_unique_resolver allow_K clenv gls) gls
+let res_pf clenv ?(with_evars=false) ?(allow_K=false) gls =
+  clenv_refine with_evars (clenv_unique_resolver allow_K clenv gls) gls
 
 let elim_res_pf_THEN_i clenv tac gls =  
   let clenv' = (clenv_unique_resolver true clenv gls) in
-  tclTHENLASTn (clenv_refine clenv') (tac clenv') gls
-
-
-let e_res_pf clenv gls =
-  clenv_refine (evar_clenv_unique_resolver clenv gls) gls
-
+  tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls
 
+let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false
 
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index cc75af0fc..038f84f01 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -16,11 +16,14 @@ open Sign
 open Evd
 open Clenv
 open Proof_type
+open Tacexpr
 (*i*)
 
 (* Tactics *)
 val unify : constr -> tactic
-val clenv_refine : clausenv -> tactic
-val res_pf : clausenv -> ?allow_K:bool -> tactic
-val e_res_pf : clausenv -> tactic
+val clenv_refine : evars_flag -> clausenv -> tactic
+val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> tactic
 val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
+
+(* Compatibility, use res_pf ?with_evars:true instead *)
+val e_res_pf : clausenv -> tactic
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index d68d125bd..cb62c084d 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -124,9 +124,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacExactNoCheck of 'constr
   | TacVmCastNoCheck of 'constr
   | TacApply of evars_flag * 'constr with_bindings
-  | TacElim of 'constr with_bindings * 'constr with_bindings option
+  | TacElim of evars_flag * 'constr with_bindings * 
+      'constr with_bindings option
   | TacElimType of 'constr
-  | TacCase of 'constr with_bindings
+  | TacCase of evars_flag * 'constr with_bindings
   | TacCaseType of 'constr
   | TacFix of identifier option * int
   | TacMutualFix of identifier * int * (identifier * int * 'constr) list
@@ -140,11 +141,11 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
 
   (* Derived basic tactics *)
   | TacSimpleInduction of quantified_hypothesis
-  | TacNewInduction of 'constr induction_arg list * 'constr with_bindings option
-      * intro_pattern_expr
+  | TacNewInduction of evars_flag * 'constr with_bindings induction_arg list * 
+      'constr with_bindings option * intro_pattern_expr
   | TacSimpleDestruct of quantified_hypothesis
-  | TacNewDestruct of 'constr induction_arg list * 'constr with_bindings option
-      * intro_pattern_expr
+  | TacNewDestruct of evars_flag * 'constr with_bindings induction_arg list *
+      'constr with_bindings option * intro_pattern_expr
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr