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

12 files changed, 37 insertions, 37 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index d2df855eed..dcd0ea469c 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -317,7 +317,7 @@ let refute_tac c t1 t2 p gls =
 	  [|intype;tt1;tt2|]) in
   let hid=pf_get_new_id (id_of_string "Heq") gls in
   let false_t=mkApp (c,[|mkVar hid|]) in
-    tclTHENS (true_cut (Name hid) neweq)
+    tclTHENS (assert_tac (Name hid) neweq)
       [proof_tac p; simplest_elim false_t] gls
 
 let convert_to_goal_tac c t1 t2 p gls =
@@ -329,14 +329,14 @@ let convert_to_goal_tac c t1 t2 p gls =
   let identity=mkLambda (Name x,sort,mkRel 1) in 
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
-    tclTHENS (true_cut (Name e) neweq) 
+    tclTHENS (assert_tac (Name e) neweq) 
       [proof_tac p;exact_check endt] gls
 
 let convert_to_hyp_tac c1 t1 c2 t2 p gls =
   let tt2=constr_of_term t2 in
   let h=pf_get_new_id (id_of_string "H") gls in
   let false_t=mkApp (c2,[|mkVar h|]) in
-    tclTHENS (true_cut (Name h) tt2)
+    tclTHENS (assert_tac (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
        simplest_elim false_t] gls
   
@@ -358,7 +358,7 @@ let discriminate_tac cstr p gls =
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|outtype;trivial;pred;identity;concl;injt|]) in
   let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
-    tclTHENS (true_cut (Name hid) neweq) 
+    tclTHENS (assert_tac (Name hid) neweq) 
       [proof_tac p;exact_check endt] gls
       
 (* wrap everything *)
diff --git a/contrib/fourier/fourier.ml b/contrib/fourier/fourier.ml
index afd85de0ae..dd54aea29a 100644
--- a/contrib/fourier/fourier.ml
+++ b/contrib/fourier/fourier.ml
@@ -202,4 +202,4 @@ let test2=[
 deduce test2;;
 unsolvable test2;;
 
-*)
\ No newline at end of file
+*)
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 903136ca28..52543cea11 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -153,7 +153,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
   fun g -> 
     let prov_id = pf_get_new_id hyp_id g in 
     tclTHENS
-      ((* observe_tac msg *) (forward (Some  (tclCOMPLETE tac)) (dummy_loc,Genarg.IntroIdentifier prov_id) t))
+      ((* observe_tac msg *) (assert_by (Name prov_id) t (tclCOMPLETE tac)))
       [tclTHENLIST 
       [	
 	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
@@ -429,7 +429,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		     in
 (* 		     observe_tac "rec hyp " *)
 		       (tclTHENS
-		       (assert_as true (dummy_loc, Genarg.IntroIdentifier rec_pte_id) t_x)
+		       (assert_tac (Name rec_pte_id) t_x)
 		       [
 			 (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
 (* 			observe_tac "prove rec hyp" *)
@@ -618,7 +618,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
 	fun g -> 
 	  let prov_hid = pf_get_new_id hid g in
 	  tclTHENLIST[
-	    forward None (dummy_loc,Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+	    pose_proof (Name prov_hid) (mkApp(mkVar hid,args));
 	    thin [hid];
 	    h_rename [prov_hid,hid]
 	  ] g
@@ -1546,10 +1546,9 @@ let prove_principle_for_gen
       ((* observe_tac "prove_rec_arg_acc"  *)
 	 (tclCOMPLETE
 	    (tclTHEN
-	       (forward 
-		  (Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))
-		  (dummy_loc,Genarg.IntroIdentifier wf_thm_id)
-		  (mkApp (delayed_force well_founded,[|input_type;relation|])))
+	       (assert_by (Name wf_thm_id)  
+		  (mkApp (delayed_force well_founded,[|input_type;relation|]))
+		  (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))
 	       (
 		 (* observe_tac  *)
 (* 		   "apply wf_thm"  *)
@@ -1610,10 +1609,10 @@ let prove_principle_for_gen
 	(List.rev_map (fun (na,_,_) -> Nameops.out_name na) 
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
-      (* observe_tac "" *) (forward
-	 (Some (prove_rec_arg_acc))
-	 (dummy_loc,Genarg.IntroIdentifier acc_rec_arg_id)
+      (* observe_tac "" *) (assert_by
+	 (Name acc_rec_arg_id)
  	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
+	 (prove_rec_arg_acc)
       );
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++  *)
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index 654474b320..a79b46d96b 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -358,7 +358,7 @@ let poseq_unsafe idunsafe cstr gl =
   tclTHEN
     (Tactics.letin_tac None (Name idunsafe) cstr None allClauses)
     (tclTHENFIRST 
-      (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr)) 
+      (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr)) 
       Tactics.reflexivity)
     gl
   
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index f62d70ab9a..5c8f087156 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -445,10 +445,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     in
     tclTHENSEQ
       [ observe_tac "intro args_names" (tclMAP h_intro args_names);
-	observe_tac "principle" (forward
-	  (Some (h_exact f_principle))
-	  (dummy_loc,Genarg.IntroIdentifier principle_id)
-	  princ_type);
+	observe_tac "principle" (assert_by
+	  (Name principle_id)
+	  princ_type
+	  (h_exact f_principle));
 	tclTHEN_i
 	  (observe_tac "functional_induction" (
 	     fun g -> 
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 528c276c05..100868a0e5 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -740,7 +740,6 @@ let termination_proof_header is_mes input_type ids args_id relation
 	   (observe_tac 
 	      "first assert" 
 	      (assert_tac 
-		 true (* the assert thm is in first subgoal *)
 		 (Name wf_rec_arg) 
 		 (mkApp (delayed_force acc_rel,
 			 [|input_type;relation;mkVar rec_arg_id|])
@@ -753,7 +752,6 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       (observe_tac 
 		  "second assert" 
 		  (assert_tac 
-		     true 
 		     (Name wf_thm)
 		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
 		  )
@@ -1155,7 +1153,7 @@ let rec introduce_all_values_eq cont_tac functional termine
       [] ->
        let heq2 = next_global_ident_away true heq_id ids in
 	tclTHENLIST
-	  [forward None (dummy_loc,IntroIdentifier heq2)
+	  [pose_proof (Name heq2)
              (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
            simpl_iter (onHyp heq2);
            unfold_in_hyp [((true,[1]), evaluable_of_global_reference 
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 203bc9e3dd..e59de34a48 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -67,6 +67,7 @@ let explore_tree pfs =
     | Move (bool, identifier, identifier') -> "Move"
     | Rename (identifier, identifier') -> "Rename"
     | Change_evars -> "Change_evars"
+    | Order _ -> "Order"
   in
   let pt = proof_of_pftreestate pfs in
     (* We expect 0 *)
@@ -280,8 +281,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacExact          c
     | TacExactNoCheck   c
     | TacVmCastNoCheck  c  -> depends_of_'constr c acc
-    | TacApply (_, _, [cb]) -> depends_of_'constr_with_bindings cb acc
-    | TacApply (_, _, _) -> failwith "TODO"
+    | TacApply (_, _, [cb], None) -> depends_of_'constr_with_bindings cb acc
+    | TacApply (_, _, _, _) -> failwith "TODO"
     | TacElim (_, cwb, cwbo) ->
 	depends_of_'constr_with_bindings cwb
 	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
@@ -420,6 +421,7 @@ and depends_of_prim_rule pr acc = match pr with
   | Move _                       -> acc
   | Rename _                     -> acc
   | Change_evars                 -> acc
+  | Order _                      -> acc
 
 let rec depends_of_pftree pt acc =
   match pt.ref with
diff --git a/contrib/interface/paths.ml b/contrib/interface/paths.ml
index b1244d1582..a157ca9254 100644
--- a/contrib/interface/paths.ml
+++ b/contrib/interface/paths.ml
@@ -23,4 +23,4 @@ let rec lex_smaller p1 p2 = match p1,p2 with
   [], _ -> true
 | a::tl1, b::tl2 when a < b -> true
 | a::tl1, b::tl2 when a = b -> lex_smaller tl1 tl2
-| _ -> false;;
\ No newline at end of file
+| _ -> false;;
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 65eadf13db..01747aa58f 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -171,7 +171,7 @@ let make_pbp_atomic_tactic = function
   | PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
   | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
   | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
-  | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings]))
+  | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings],None))
   | PbpElim (hyp_name, names) ->
       let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
       TacAtom
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 4b9c1332a4..cf861642db 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1202,7 +1202,8 @@ let rec natural_ntree ig ntree =
 	  | TacExtend (_,"InductionIntro",[a]) -> 
               let id=(out_gen wit_ident a) in
               natural_induction ig lh g gs ge id ltree true
-	  | TacApply (_,false,[c,_]) -> natural_apply ig lh g gs (snd c) ltree
+	  | TacApply (_,false,[c,_],None) ->
+              natural_apply ig lh g gs (snd c) ltree
 	  | TacExact c -> natural_exact ig lh g gs (snd c) ltree
 	  | TacCut c -> natural_cut ig lh g gs (snd c) ltree
 	  | TacExtend (_,"CutIntro",[a]) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 8ec6cfb2f4..b404478ffb 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1163,12 +1163,12 @@ and xlate_tac =
 	xlate_error "TODO: trivial using"
     | TacReduce (red, l) ->
      CT_reduce (xlate_red_tactic red, xlate_clause l)
-    | TacApply (true,false,[c,bindl]) ->
+    | TacApply (true,false,[c,bindl],None) ->
      CT_apply (xlate_formula c, xlate_bindings bindl)
-    | TacApply (true,true,[c,bindl]) ->
+    | TacApply (true,true,[c,bindl],None) ->
      CT_eapply (xlate_formula c, xlate_bindings bindl)
-    | TacApply (_,_,_) ->
-	xlate_error "TODO: simple (e)apply and iterated apply"
+    | TacApply (_,_,_,_) ->
+	xlate_error "TODO: simple (e)apply and iterated apply and apply in"
     | TacConstructor (false,n_or_meta, bindl) ->
 	let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
 	in CT_constructor (CT_int n, xlate_bindings bindl)
@@ -1256,13 +1256,13 @@ and xlate_tac =
 		     but the structures are different *)
 		  xlate_clause cl)
     | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
-    | TacAssert (None, (_,IntroIdentifier id), c) -> 
+    | TacAssert (None, Some (_,IntroIdentifier id), c) -> 
         CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
-    | TacAssert (None, (_,IntroAnonymous), c) -> 
+    | TacAssert (None, None, c) -> 
         CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
-    | TacAssert (Some (TacId []), (_,IntroIdentifier id), c) -> 
+    | TacAssert (Some (TacId []), Some (_,IntroIdentifier id), c) -> 
         CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
-    | TacAssert (Some (TacId []), (_,IntroAnonymous), c) -> 
+    | TacAssert (Some (TacId []), None, c) -> 
         CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
     | TacAssert _ ->
 	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 920b33b7a5..4079b0f200 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -232,7 +232,7 @@ let build_dependent_sum l =
 	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
 	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
 	   with _ -> ());
-	let tac = assert_tac true (Name n) hyptype in
+	let tac = assert_tac (Name n) hyptype in
 	let conttac = 
 	  (fun cont -> 
 	     conttac