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

1 files changed, 4 insertions, 4 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index e798d87554..a17ea69fed 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -536,7 +536,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 *)
                     tclREPEAT (
                       tclTHENSEQ [
-                         apply_in false freshz [(andb_prop()),Rawterm.NoBindings] None;
+                         apply_in false false freshz [(Evd.empty,andb_prop()),Rawterm.NoBindings] None;
                          fun gl ->
                            let fresht = fresh_id (!avoid) (id_of_string "Z") gsig 
                            in
@@ -748,8 +748,8 @@ let compute_dec_tact ind lnamesparrec nparrec =
       Pfedit.by ( tclTHENSEQ [
                         intros_using fresh_first_intros;
                         intros_using [freshn;freshm];
-                        assert_as true (dl,Genarg.IntroIdentifier freshH) (
-                    mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
+                        assert_tac (Name freshH) (
+                        mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
                   ) ]); 
 (*we do this so we don't have to prove the same goal twice *)
       Pfedit.by (  tclTHEN 
@@ -795,7 +795,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
                       unfold_constr (Lazy.force Coqlib.coq_not_ref);
                       intro;
                       Equality.subst_all;
-                assert_as true (dl,Genarg.IntroIdentifier freshH3) 
+                assert_tac (Name freshH3) 
                 (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
           ]);
           Pfedit.by