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

4 files changed, 15 insertions, 18 deletions

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