Fix a bug reintroduced in [setoid_reflexivity] etc...

Go back to refine_hyp instead of specialize, because only the former
handles open terms.


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

1 files changed, 15 insertions, 0 deletions

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 9cb7725c0..5c904e219 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -233,6 +233,21 @@ 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. *)