More debugging of [Equations], now able to discharge even the heavily

dependent [noConfusion] definitions in "A Few Constructions on
Constructors". Now the guardness check is blocking.


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

1 files changed, 20 insertions, 15 deletions

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 7fe5211af..9cb7725c0 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -121,6 +121,26 @@ Ltac on_application f tac T :=
     | context [f ?x ?y] => tac (f x y) 
     | context [f ?x] => tac (f x)
   end.
+
+(** A variant of [apply] using [refine], doing as much conversion as necessary. *)
+
+Ltac rapply p := 
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _) ||
+  refine (p _ _ _ _) ||
+  refine (p _ _ _) ||
+  refine (p _ _) ||
+  refine (p _) ||
+  refine p.
   
 (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *)
 
@@ -213,21 +233,6 @@ Ltac replace_hyp H c :=
   let H' := fresh "H" in
     assert(H' := c) ; clear H ; rename H' into H.
 
-(** A tactic to refine an hypothesis by supplying some of its arguments. *)
-
-Ltac refine_hyp c :=
-  let tac H := replace_hyp H c in
-    match c with
-      | ?H _ => tac H
-      | ?H _ _ => tac H
-      | ?H _ _ _ => tac H
-      | ?H _ _ _ _ => tac H
-      | ?H _ _ _ _ _ => tac H
-      | ?H _ _ _ _ _ _ => tac H
-      | ?H _ _ _ _ _ _ _ => tac H
-      | ?H _ _ _ _ _ _ _ _ => tac H
-    end.
-
 (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto]
    is not enough, better rebind using [Obligation Tactic := tac] in this case, 
    possibly using [program_simplify] to use standard goal-cleaning tactics. *)