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

1 files changed, 16 insertions, 7 deletions

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;