Add support for remaining side-conditions in "apply in as".

Tolerate that the place where to move an hypothesis with destruct is not
"safe" if the lemma has dependent parameters inferred lately.



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

3 files changed, 29 insertions, 8 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index eddf387f9..0fbd8ad21 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -262,7 +262,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
 	    if with_dep & hto <> MoveAfter hyp then
 	      (first, d::middle)
             else
-	      errorlabstrm "" (str "Cannot move " ++ pr_id idfrom ++
+	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++
 	        pr_move_location pr_id hto ++
 	        str (if toleft then ": it occurs in " else ": it depends on ")
 	        ++ pr_id hyp ++ str ".")
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f4262d731..b2f7a4374 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1320,7 +1320,7 @@ let rec intros_patterns b avoid thin destopt = function
         (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l))
 	  no_move true false)
         (onLastHypId (fun id ->
-	  tclTHEN
+	  tclTHENLAST (* Skip the side conditions of the rewriting step *)
 	    (rewrite_hyp l2r id)
 	    (intros_patterns b avoid thin destopt l)))
   | [] -> clear_wildcards thin
@@ -1393,7 +1393,7 @@ let as_tac id ipat = match ipat with
   | None -> tclIDTAC
 
 let general_apply_in with_delta with_destruct with_evars id lemmas ipat gl =
-  tclTHEN
+  tclTHENFIRST (* Skip the side conditions of the applied lemma *)
     (tclMAP (apply_in_once with_delta with_destruct with_evars id) lemmas)
     (as_tac id ipat)
     gl
@@ -1758,6 +1758,15 @@ let re_intro_dependent_hypotheses (lstatus,rstatus) tophyp =
 
 let update destopt tophyp = if destopt = no_move then tophyp else destopt
 
+let safe_dest_intros_patterns avoid dest pat gl =
+  try intros_patterns true avoid [] dest pat gl
+  with UserError ("move_hyp",_) ->
+    (* May happen if the lemma has dependent arguments that has resolved
+       only after cook_sign is called, e.g. as in 
+       "dec:forall x, {x=0}+{x<>0};  a:A  |- if dec a then True else False"
+       for argument a of dec which will be found only lately *)
+    intros_patterns true avoid [] no_move pat gl
+
 type elim_arg_kind = RecArg | IndArg | OtherArg
 
 let induct_discharge destopt avoid' tac (avoid,ra) names gl =
@@ -1780,23 +1789,23 @@ let induct_discharge destopt avoid' tac (avoid,ra) names gl =
 	  if tophyp=no_move then first_name_buggy avoid gl hyprec else tophyp
 	in
         tclTHENLIST
-	  [ intros_patterns true avoid [] (update destopt tophyp) [recpat];
-	    intros_patterns true avoid [] no_move [hyprec];
+	  [ safe_dest_intros_patterns avoid (update destopt tophyp) [recpat];
+	    safe_dest_intros_patterns avoid no_move [hyprec];
 	    peel_tac ra' names newtophyp] gl
     | (IndArg,dep,hyprecname) :: ra' ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
         let pat,names = consume_pattern avoid hyprecname dep gl names in
-	tclTHEN (intros_patterns true avoid [] (update destopt tophyp) [pat])
+	tclTHEN (safe_dest_intros_patterns avoid (update destopt tophyp) [pat])
           (peel_tac ra' names tophyp) gl
     | (RecArg,dep,recvarname) :: ra' ->
         let pat,names = consume_pattern avoid recvarname dep gl names in
-	tclTHEN (intros_patterns true avoid [] (update destopt tophyp) [pat])
+	tclTHEN (safe_dest_intros_patterns avoid (update destopt tophyp) [pat])
           (peel_tac ra' names tophyp) gl
     | (OtherArg,_,_) :: ra' ->
         let pat,names = match names with
           | [] -> (dloc, IntroAnonymous), []
           | pat::names -> pat,names in
-	tclTHEN (intros_patterns true avoid [] (update destopt tophyp) [pat])
+	tclTHEN (safe_dest_intros_patterns avoid (update destopt tophyp) [pat])
           (peel_tac ra' names tophyp) gl
     | [] ->
         check_unused_names names;
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 8014f73fc..c3d3b0e3b 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -284,3 +284,15 @@ Proof.
 eexists; intros x H.
 apply H.
 Qed.
+
+(* Check that "as" clause applies to main premise only and leave the
+   side conditions away *)
+
+Lemma side_condition : 
+  forall (A:Type) (B:Prop) x, (True -> B -> x=0) -> B -> x=x.
+Proof.
+intros.
+apply H in H0 as ->.
+reflexivity.
+exact I.
+Qed.