Ajout "simple apply" et "simple eapply" pour apply sans unfold

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

5 files changed, 31 insertions, 18 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 60f1ccf0ca..18263127be 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -39,9 +39,9 @@ let h_exact_no_check c =
   abstract_tactic (TacExactNoCheck (inj_open c)) (exact_no_check c)
 let h_vm_cast_no_check c = 
   abstract_tactic (TacVmCastNoCheck (inj_open c)) (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_apply simple ev cb    =
+  abstract_tactic (TacApply (simple,ev,inj_open_wb cb))
+    (apply_with_ebindings_gen simple ev cb)
 let h_elim ev cb cbo    =
   abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo))
     (elim ev cb cbo)
@@ -123,8 +123,8 @@ let h_symmetry c     = abstract_tactic (TacSymmetry c) (intros_symmetry c)
 let h_transitivity c =
   abstract_tactic (TacTransitivity (inj_open c)) (intros_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_apply c  = h_apply false false (c,NoBindings)
+let h_simplest_eapply c = h_apply false true (c,NoBindings)
 let h_simplest_elim c   = h_elim false (c,NoBindings) None
 let h_simplest_case   c = h_case false (c,NoBindings)
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 909d294cf6..84a5719374 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -34,7 +34,8 @@ val h_exact           : constr -> tactic
 val h_exact_no_check  : constr -> tactic
 val h_vm_cast_no_check  : constr -> tactic
 
-val h_apply           : evars_flag -> constr with_ebindings -> tactic
+val h_apply           : advanced_flag -> evars_flag -> 
+                        constr with_ebindings -> tactic
 
 val h_elim            : evars_flag -> constr with_ebindings ->
                         constr with_ebindings option -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 536b5ebbdf..719307b116 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -645,7 +645,7 @@ let rec intern_atomic lf ist x =
   | TacExact c -> TacExact (intern_constr ist c)
   | 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)
+  | TacApply (a,ev,cb) -> TacApply (a,ev,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)
@@ -2002,7 +2002,7 @@ and interp_atomic ist gl = function
   | TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
   | 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)
+  | TacApply (a,ev,cb) -> h_apply a ev (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)
@@ -2336,7 +2336,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacExact c -> TacExact (subst_rawconstr subst c)
   | 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)
+  | TacApply (a,ev,cb) -> TacApply (a,ev,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)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e8192c177e..28e35cf97b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -545,7 +545,9 @@ let clenv_refine_in with_evars id clenv gl =
 
 (* Resolution with missing arguments *)
 
-let apply_with_ebindings_gen with_evars (c,lbind) gl = 
+let apply_with_ebindings_gen advanced with_evars (c,lbind) gl =
+  let flags = 
+    if advanced 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. *)
@@ -555,7 +557,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
-    Clenvtac.res_pf clause ~with_evars:with_evars gl in
+    Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in
   try try_apply thm_ty0 concl_nprod
   with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->
     let rec try_red_apply thm_ty =
@@ -573,14 +575,17 @@ let apply_with_ebindings_gen with_evars (c,lbind) gl =
         else raise exn in
     try_red_apply thm_ty0
 
-let apply_with_ebindings = apply_with_ebindings_gen false
-let eapply_with_ebindings = apply_with_ebindings_gen true
+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 = apply_with_ebindings_gen false false
+let eapply_with_ebindings = apply_with_ebindings_gen false true
 
 let apply_with_bindings (c,bl) =
   apply_with_ebindings (c,inj_ebindings bl)
 
 let eapply_with_bindings (c,bl) =
-  apply_with_ebindings_gen true (c,inj_ebindings bl)
+  apply_with_ebindings_gen false true (c,inj_ebindings bl)
 
 let apply c =
   apply_with_ebindings (c,NoBindings)
@@ -589,7 +594,7 @@ let apply_list = function
   | c::l -> apply_with_bindings (c,ImplicitBindings l)
   | _ -> assert false
 
-(* Resolution with no reduction on the type *)
+(* Resolution with no reduction on the type (used ?) *)
 
 let apply_without_reduce c gl = 
   let clause = mk_clenv_type_of gl c in 
@@ -796,7 +801,7 @@ let constructor_tac expctdnumopt i lbind gl =
     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 = apply_with_ebindings (cons,lbind) in
+  let apply_tac = advanced_apply_with_ebindings (cons,lbind) in
   (tclTHENLIST 
      [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c723c2b9a3..084aba9efa 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -172,12 +172,19 @@ val bring_hyps : named_context -> tactic
 val apply                 : constr      -> tactic
 val apply_without_reduce  : constr      -> tactic
 val apply_list            : constr list -> tactic
-val apply_with_ebindings_gen : evars_flag -> constr with_ebindings -> tactic
+
+val apply_with_ebindings_gen : 
+  advanced_flag -> evars_flag -> constr with_ebindings -> tactic
+
 val apply_with_bindings   : constr with_bindings -> tactic
-val apply_with_ebindings  : constr with_ebindings -> tactic
 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