About "apply in":

- Added "simple apply in" (cf wish 1917) + conversion and descent
  under conjunction + contraction of useless beta-redex in "apply in"
  + support for open terms.
- Did not solve the "problem" that "apply in" generates a let-in which
  is type-checked using a kernel conversion in the opposite side of what
  the proof indicated (hence leading to a potential unexpected penalty
  at Qed time).
- When applyng a sequence of lemmas, it would have been nice to allow
  temporary evars as intermediate steps but this was too long to implement.

Smoother API in tactics.mli for assert_by/assert_as/pose_proof.



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

11 files changed, 133 insertions, 103 deletions

diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 299e3fd17b..741874cb31 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -107,7 +107,7 @@ let clean_tmp gls =
     clean_all (tmp_ids gls) gls
 
 let assert_postpone id t =
-  assert_as true (dummy_loc, Genarg.IntroIdentifier id) t
+  assert_tac (Name id) t
 
 (* start a proof *)
 
@@ -780,7 +780,7 @@ let consider_tac c hyps gls =
     | _ -> 
 	let id = pf_get_new_id (id_of_string "_tmp") gls in
 	tclTHEN 
-	  (forward None (dummy_loc, Genarg.IntroIdentifier id) c)
+	  (forward None (Some (dummy_loc, Genarg.IntroIdentifier id)) c)
  	  (consider_match false [] [id] hyps) gls 
 	  
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e3914b8c51..eba3a119f2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -272,7 +272,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl =
     let e = build_coq_eq () in
     let sym = build_coq_sym_eq () in
     let eq = applist (e, [t1;c1;c2]) in
-    tclTHENS (assert_tac false Anonymous eq)
+    tclTHENS (assert_as false None eq)
       [onLastHyp (fun id -> 
 	tclTHEN 
 	  (tclTRY (general_multi_rewrite false false (inj_open (mkVar id),NoBindings) clause))
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 845483436f..62ac0d4d72 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -486,23 +486,6 @@ END
 
 
 
-TACTIC EXTEND apply_in
-| ["apply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] -> 
-    [ apply_in false id cl None ]
-| ["apply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) 
-   "as" simple_intropattern(ipat) ] -> 
-    [ apply_in false id cl (Some ipat) ]
-END
-
-
-TACTIC EXTEND eapply_in
-| ["eapply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] ->
-    [ apply_in true id cl None ]
-| ["eapply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) 
-   "as" simple_intropattern(ipat) ] -> 
-    [ apply_in true id cl (Some ipat) ]
-END
-
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as 
   defined by Conor McBride *)
 TACTIC EXTEND generalize_eqs
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 6498c35429..c9992c36ff 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -39,9 +39,12 @@ 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 simple ev cb    =
-  abstract_tactic (TacApply (simple,ev,cb))
+let h_apply simple ev cb =
+  abstract_tactic (TacApply (simple,ev,cb,None))
     (apply_with_ebindings_gen simple ev cb)
+let h_apply_in simple ev cb (id,ipat as inhyp) =
+  abstract_tactic (TacApply (simple,ev,cb,Some inhyp))
+    (apply_in simple ev id cb ipat)
 let h_elim ev cb cbo    =
   abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo))
     (elim ev cb cbo)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 851c33e7a8..faa8c4150d 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -39,6 +39,9 @@ val h_vm_cast_no_check  : constr -> tactic
 
 val h_apply           : advanced_flag -> evars_flag -> 
   open_constr with_bindings list -> tactic
+val h_apply_in        : advanced_flag -> evars_flag -> 
+  open_constr with_bindings list -> 
+  identifier * intro_pattern_expr located option -> tactic
 
 val h_elim            : evars_flag -> constr with_ebindings ->
                         constr with_ebindings option -> tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index e0ed2d1ef4..b6923bb83f 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -469,7 +469,7 @@ let raw_inversion inv_kind id status names gl =
       case_nodep_then_using 
   in
   (tclTHENS
-     (true_cut Anonymous cut_concl)
+     (assert_tac Anonymous cut_concl)
      [case_tac names 
        (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
        (Some elim_predicate) ([],[]) ind indclause;
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 9225fd9d7c..88038a88ed 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -314,7 +314,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
        because of evars limitation, use non dependent assert instead *)
     | LetIn (Name id,c1,t1,c2), _ ->
 	tclTHENS
-          (assert_tac true (Name id) t1) 
+          (assert_tac (Name id) t1) 
 	  [(match List.hd sgp with 
 	     | None -> tclIDTAC
 	     | Some th -> onLastHyp (fun id -> tcc_aux (mkVar id::subst) th));
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 644a68666a..f74d6dfdfb 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1917,7 +1917,7 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_
     let eq_left_to_right = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c1 ; c2 ])) in
     let eq_right_to_left = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c2 ; c1 ])) in
     let replace dir eq =
-      tclTHENS (assert_tac false Anonymous eq)
+      tclTHENS (assert_as false None eq)
 	[onLastHyp (fun id ->
           tclTHEN
             (rewrite_tac dir all_occurrences (mkVar id) ~new_goals)
@@ -1929,7 +1929,7 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_
   with
       Optimize -> (* (!replace tac_opt c1 c2) gl *)
 	let eq =  mkApp (Lazy.force  coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in 
-	  tclTHENS (assert_tac false Anonymous eq)
+	  tclTHENS (assert_as false None eq)
 	    [onLastHyp (fun id ->
 	      tclTHEN
 		(rewrite_tac false all_occurrences (mkVar id) ~new_goals)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e89672e513..bf05341678 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -596,20 +596,24 @@ let intern_red_expr ist = function
   | Simpl o -> Simpl (Option.map (intern_constr_with_occurrences ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r
   
+let intern_in_hyp_as ist lf (id,ipat) =
+  (intern_hyp_or_metaid ist id, Option.map (intern_intro_pattern lf ist) ipat)
+
+let intern_hyp_list ist = List.map (intern_hyp_or_metaid ist)
 
 let intern_inversion_strength lf ist = function
   | NonDepInversion (k,idl,ids) ->
-      NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl,
+      NonDepInversion (k,intern_hyp_list ist idl,
       Option.map (intern_intro_pattern lf ist) ids)
   | DepInversion (k,copt,ids) ->
       DepInversion (k, Option.map (intern_constr ist) copt,
       Option.map (intern_intro_pattern lf ist) ids)
   | InversionUsing (c,idl) ->
-      InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
+      InversionUsing (intern_constr ist c, intern_hyp_list ist idl)
 
 (* Interprets an hypothesis name *)
 let intern_hyp_location ist (((b,occs),id),hl) =
-  (((b,List.map (intern_or_var ist) occs),intern_hyp ist (skip_metaid id)), hl)
+  (((b,List.map (intern_or_var ist) occs),intern_hyp_or_metaid ist id), hl)
 
 let interp_constrpattern_gen sigma env ?(as_type=false) ltacvar c =
   let c = intern_gen as_type ~allow_patvar:true ~ltacvars:(ltacvar,[])
@@ -704,8 +708,9 @@ 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 (a,ev,cb) ->
-      TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb)
+  | TacApply (a,ev,cb,inhyp) ->
+      TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb,
+                Option.map (intern_in_hyp_as ist lf) inhyp)
   | TacElim (ev,cb,cbo) ->
       TacElim (ev,intern_constr_with_bindings ist cb,
                Option.map (intern_constr_with_bindings ist) cbo)
@@ -723,7 +728,7 @@ let rec intern_atomic lf ist x =
   | TacCut c -> TacCut (intern_type ist c)
   | TacAssert (otac,ipat,c) ->
       TacAssert (Option.map (intern_tactic ist) otac,
-                 intern_intro_pattern lf ist ipat,
+                 Option.map (intern_intro_pattern lf ist) ipat,
                  intern_constr_gen (otac<>None) ist c)
   | TacGeneralize cl ->
       TacGeneralize (List.map (fun (c,na) ->
@@ -1659,6 +1664,9 @@ let rec interp_intro_pattern ist gl = function
 and interp_or_and_intro_pattern ist gl =
   List.map (List.map (interp_intro_pattern ist gl))
 
+let interp_in_hyp_as ist gl (id,ipat) =
+  (interp_hyp ist gl id,Option.map (interp_intro_pattern ist gl) ipat)
+
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
 let coerce_to_quantified_hypothesis = function
@@ -2186,8 +2194,11 @@ 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 (a,ev,cb) ->
+  | TacApply (a,ev,cb,None) ->
       h_apply a ev (List.map (interp_open_constr_with_bindings ist gl) cb)
+  | TacApply (a,ev,cb,Some cl) ->
+      h_apply_in a ev (List.map (interp_open_constr_with_bindings ist gl) cb)
+        (interp_in_hyp_as ist gl cl)
   | TacElim (ev,cb,cbo) ->
       h_elim ev (interp_constr_with_bindings ist gl cb)
                 (Option.map (interp_constr_with_bindings ist gl) cbo)
@@ -2207,7 +2218,7 @@ and interp_atomic ist gl = function
       let c = (if t=None then interp_constr else interp_type) ist (project gl) (pf_env gl) c in
       abstract_tactic (TacAssert (t,ipat,inj_open c))
         (Tactics.forward (Option.map (interp_tactic ist) t)
-	  (interp_intro_pattern ist gl ipat) c)
+	  (Option.map (interp_intro_pattern ist gl) ipat) c)
   | TacGeneralize cl ->
       h_generalize_gen
         (pf_interp_constr_with_occurrences_and_name_as_list ist gl cl)
@@ -2523,8 +2534,8 @@ 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 (a,ev,cb) ->
-      TacApply (a,ev,List.map (subst_raw_with_bindings subst) cb)
+  | TacApply (a,ev,cb,cl) ->
+      TacApply (a,ev,List.map (subst_raw_with_bindings subst) cb,cl)
   | 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 b4371ac23a..3511585d51 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -566,17 +566,11 @@ let cut c gl =
 
 let cut_intro t = tclTHENFIRST (cut t) intro
 
-(* let cut_replacing id t tac = 
-  tclTHENS (cut t)
-    [tclORELSE
-	(intro_replacing id) 
-	(tclORELSE (intro_erasing id) (intro_using id));
-     tac (refine_no_check (mkVar id)) ] *)
-
 (* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le
    but, ou dans une autre hypothèse *)
 let cut_replacing id t tac = 
-  tclTHENS (cut t) [ intro_replacing id; tac (refine_no_check (mkVar id)) ]
+  tclTHENLAST (internal_cut_rev_replace id t)
+    (tac (refine_no_check (mkVar id)))
 
 let cut_in_parallel l = 
   let rec prec = function
@@ -729,32 +723,54 @@ let general_case_analysis with_evars (c,lbindc as cx) =
 
 let simplest_case c = general_case_analysis false (c,NoBindings)
 
+(* Apply a tactic below the products of the conclusion of a lemma *) 
+
+let descend_in_conjunctions tac exit c gl =
+  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 _ ->
+	let n = (mis_constr_nargs mind).(0) in
+	let sort = elimination_sort_of_goal gl in
+	let elim = pf_apply make_case_gen gl mind sort in
+	tclTHENLAST
+	  (general_elim true (c,NoBindings) (elim,NoBindings))
+	  (tclTHENLIST [
+	    tclDO n intro;
+	    tclLAST_NHYPS n (fun l ->
+	      tclFIRST
+		(List.map (fun id -> tclTHEN (tac (mkVar id)) (thin l)) l))])
+          gl
+    | None ->
+	raise Exit
+  with RefinerError _|UserError _|Exit -> exit ()
+
 (****************************************************)
 (*            Resolution tactics                    *)
 (****************************************************)
 
 (* Resolution with missing arguments *)
 
-let general_apply with_delta with_destruct with_evars (c,lbind) gl =
+let check_evars sigma evm gl =
+  let origsigma = gl.sigma in
+  let rest = 
+    Evd.fold (fun ev evi acc -> 
+      if not (Evd.mem origsigma ev) && not (Evd.is_defined sigma ev) 
+      then Evd.add acc ev evi else acc)
+      evm Evd.empty
+  in 
+  if rest <> Evd.empty then
+    errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ 
+      fnl () ++ pr_evar_map rest)
+
+let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
   let flags = 
     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. *)
-  let concl_nprod = nb_prod (pf_concl gl) in
+  let concl_nprod = nb_prod (pf_concl gl0) in
   let evm, c = c in
-  let origsigm = gl.sigma in
-  let check_evars sigm =
-    let rest = 
-      Evd.fold (fun ev evi acc -> 
-	if Evd.mem sigm ev && not (Evd.mem origsigm ev) && not (Evd.is_defined sigm ev) then
-	  Evd.add acc ev evi
-	else acc) evm Evd.empty
-    in 
-      if not (rest = Evd.empty) then
-	errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ fnl () ++
-				 pr_evar_map rest)
-  in
   let rec try_main_apply c gl =
     let thm_ty0 = nf_betaiota (pf_type_of gl c) in
     let try_apply thm_ty nprod =
@@ -762,7 +778,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl =
 	if n<0 then error "Applied theorem has not enough premisses.";
 	let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
 	let res = Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in
-	  if not with_evars then check_evars (fst res).sigma; 
+	  if not with_evars then check_evars (fst res).sigma evm gl0;
 	  res
     in
       try try_apply thm_ty0 concl_nprod
@@ -780,32 +796,15 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl =
 	    try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit
 	    with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
 	      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 _ ->
-			let n = (mis_constr_nargs mind).(0) in
-			let sort = elimination_sort_of_goal gl in
-			let elim = pf_apply make_case_gen gl mind sort in
-			  tclTHENLAST
-			    (general_elim with_evars (c,NoBindings) (elim,NoBindings))
-			    (tclTHENLIST [
-			      tclDO n intro;
-			      tclLAST_NHYPS n (fun l ->
-				tclFIRST
-				  (List.map (fun id ->
-				    tclTHEN (try_main_apply (mkVar id)) (thin l)) l))
-			    ]) gl
-		    | None ->
-			raise Exit
-		with RefinerError _|UserError _|Exit -> raise exn 
+                descend_in_conjunctions 
+                  try_main_apply (fun _ -> raise exn) c gl
 	      else
 		raise exn
 	in try_red_apply thm_ty0 
   in
-    if evm = Evd.empty then try_main_apply c gl
+    if evm = Evd.empty then try_main_apply c gl0
     else
-      tclTHEN (tclEVARS (Evd.merge gl.sigma evm)) (try_main_apply c) gl
+      tclTHEN (tclEVARS (Evd.merge gl0.sigma evm)) (try_main_apply c) gl0
 
 let rec apply_with_ebindings_gen b e = function
   | [] ->
@@ -855,21 +854,43 @@ let find_matching_clause unifier clause =
     with NotExtensibleClause -> failwith "Cannot apply"
   in find clause
 
-let progress_with_clause innerclause clause =
+let progress_with_clause flags innerclause clause =
   let ordered_metas = List.rev (clenv_independent clause) in
   if ordered_metas = [] then error "Statement without assumptions.";
-  let f mv = find_matching_clause (clenv_fchain mv clause) innerclause in
+  let f mv =
+    find_matching_clause (clenv_fchain mv ~flags clause) innerclause in
   try list_try_find f ordered_metas
   with Failure _ -> error "Unable to unify."
 
-let apply_in_once gl innerclause (d,lbind) =
+let apply_in_once_main flags innerclause (d,lbind) gl =
   let thm = nf_betaiota (pf_type_of gl d) in
   let rec aux clause =
-    try progress_with_clause innerclause clause
+    try progress_with_clause flags innerclause clause
     with err ->
     try aux (clenv_push_prod clause)
-    with NotExtensibleClause -> raise err
-  in aux (make_clenv_binding gl (d,thm) lbind)
+    with NotExtensibleClause -> raise err in 
+  aux (make_clenv_binding gl (d,thm) lbind)
+
+let apply_in_once with_delta with_destruct with_evars id ((sigma,d),lbind) gl0 =
+  let flags = 
+    if with_delta then default_unify_flags else default_no_delta_unify_flags in
+  let t' = pf_get_hyp_typ gl0 id in
+  let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in
+  let rec aux c gl =
+    try
+      let clause = apply_in_once_main flags innerclause (c,lbind) gl in
+      let res = clenv_refine_in with_evars id clause gl in
+      if not with_evars then check_evars (fst res).sigma sigma gl0;
+      res
+    with exn when with_destruct ->
+      descend_in_conjunctions aux (fun _ -> raise exn) c gl
+  in
+    if sigma = Evd.empty then aux d gl0
+    else
+      tclTHEN (tclEVARS (Evd.merge gl0.sigma sigma)) (aux d) gl0
+
+
+
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
    |- B -> C and |- A
@@ -1200,7 +1221,9 @@ let intro_patterns = function
 
 let make_id s = fresh_id [] (default_id_of_sort s)
 
-let prepare_intros s (loc,ipat) gl = match ipat with
+let prepare_intros s ipat gl = match ipat with
+  | None -> make_id s gl, tclIDTAC
+  | Some (loc,ipat) -> match ipat with
   | IntroIdentifier id -> id, tclIDTAC
   | IntroAnonymous -> make_id s gl, tclIDTAC
   | IntroFresh id -> fresh_id [] id gl, tclIDTAC
@@ -1212,11 +1235,11 @@ let prepare_intros s (loc,ipat) gl = match ipat with
       intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
 
 let ipat_of_name = function
-  | Anonymous -> IntroAnonymous
-  | Name id -> IntroIdentifier id
+  | Anonymous -> None
+  | Name id -> Some (dloc, IntroIdentifier id)
 
 let allow_replace c gl = function (* A rather arbitrary condition... *)
-  | _, IntroIdentifier id ->
+  | Some (_, IntroIdentifier id) ->
       fst (decompose_app (snd (decompose_lam_assum c))) = mkVar id
   | _ ->
       false
@@ -1231,8 +1254,7 @@ let assert_as first ipat c gl =
 	(if first then [tclIDTAC; tac] else [tac; tclIDTAC]) gl
   | _  -> error "Not a proposition or a type."
 
-let assert_tac first na = assert_as first (dloc,ipat_of_name na)
-let true_cut = assert_tac true 
+let assert_tac na = assert_as true (ipat_of_name na)
 
 (* apply in as *)
 
@@ -1246,12 +1268,13 @@ let as_tac id ipat = match ipat with
       user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected")
   | None -> tclIDTAC
 
-let apply_in with_evars id lemmas ipat gl =
-  let t' = pf_get_hyp_typ gl id in
-  let innermostclause = mk_clenv_from_n gl (Some 0) (mkVar id,t') in
-  let clause = List.fold_left (apply_in_once gl) innermostclause lemmas in
-  tclTHEN (clenv_refine_in with_evars id clause) (as_tac id ipat)
- gl
+let general_apply_in with_delta with_destruct with_evars id lemmas ipat gl =
+  tclTHEN
+    (tclMAP (apply_in_once with_delta with_destruct with_evars id) lemmas)
+    (as_tac id ipat)
+    gl
+
+let apply_in simple with_evars = general_apply_in simple simple with_evars
 
 (**************************)
 (*   Generalize tactics   *)
@@ -1499,6 +1522,9 @@ let forward usetac ipat c gl =
   | Some tac -> 
       tclTHENFIRST (assert_as true ipat c) tac gl
 
+let pose_proof na c = forward None (ipat_of_name na) c
+let assert_by na t tac = forward (Some tac) (ipat_of_name na) t
+
 (*****************************)
 (* Ad hoc unfold             *)
 (*****************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f18860af42..050473bfec 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -193,7 +193,9 @@ val eapply_with_ebindings : open_constr with_ebindings -> tactic
 
 val cut_and_apply         : constr -> tactic
 
-val apply_in : evars_flag -> identifier -> constr with_ebindings list ->
+val apply_in : 
+  advanced_flag -> evars_flag -> identifier -> 
+  open_constr with_ebindings list ->
   intro_pattern_expr located option -> tactic
 
 (*s Elimination tactics. *)
@@ -344,12 +346,14 @@ val cut_replacing               :
   identifier -> constr -> (tactic -> tactic) -> tactic
 val cut_in_parallel             : constr list -> tactic
 
-val assert_as : bool -> intro_pattern_expr located -> constr -> tactic
-val forward   : tactic option -> intro_pattern_expr located -> constr -> tactic
+val assert_as : bool -> intro_pattern_expr located option -> constr -> tactic
+val forward   : tactic option -> intro_pattern_expr located option -> constr -> tactic
 val letin_tac : (bool * intro_pattern_expr located) option -> name -> 
   constr -> types option -> clause -> tactic
-val true_cut                    : name -> constr -> tactic
-val assert_tac                  : bool -> name -> constr -> tactic
+val assert_tac : name -> types -> tactic
+val assert_by  : name -> types -> tactic -> tactic
+val pose_proof : name -> constr -> tactic
+
 val generalize      : constr list -> tactic
 val generalize_gen  : ((occurrences * constr) * name) list -> tactic
 val generalize_dep  : constr  -> tactic