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

3 files changed, 39 insertions, 19 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e803e8dcbc..22e95ef5d8 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1734,14 +1734,20 @@ let relation_of_constr env c =
 	
 let setoid_proof gl ty fn fallback =
   let env = pf_env gl in
-  let rel, args = relation_of_constr env (pf_concl gl) in
-  let evm, car = project gl, pf_type_of gl args.(0) in
-    try fn env evm car rel gl
-    with Not_found -> 
+    try 
+      let rel, args = relation_of_constr env (pf_concl gl) in
+      let evm, car = project gl, pf_type_of gl args.(0) in
+	fn env evm car rel gl
+    with e -> 
       match fallback gl with
       | Some tac -> tac gl
-      | None -> not_declared env ty rel gl
-	  
+      | None -> 
+	  match e with
+	  | Not_found ->
+	      let rel, args = relation_of_constr env (pf_concl gl) in
+		not_declared env ty rel gl
+	  | _ -> raise e
+	      
 let setoid_reflexivity gl =
   setoid_proof gl "reflexive" 
     (fun env evm car rel -> apply (get_reflexive_proof env evm car rel))
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 3e0e8ca2be..11f710997e 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -189,33 +189,32 @@ Ltac simplify_eqs :=
 (** A tactic that tries to remove trivial equality guards in induction hypotheses coming
    from [dependent induction]/[generalize_eqs] invocations. *)
 
-
 Ltac simpl_IH_eq H :=
   match type of H with
     | @JMeq _ ?x _ _ -> _ =>
-      specialize (H (JMeq_refl x))
+      refine_hyp (H (JMeq_refl x))
     | _ -> @JMeq _ ?x _ _ -> _ =>
-      specialize (H _ (JMeq_refl x))
+      refine_hyp (H _ (JMeq_refl x))
     | _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      specialize (H _ _ (JMeq_refl x))
+      refine_hyp (H _ _ (JMeq_refl x))
     | _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      specialize (H _ _ _ (JMeq_refl x))
+      refine_hyp (H _ _ _ (JMeq_refl x))
     | _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      specialize (H _ _ _ _ (JMeq_refl x))
+      refine_hyp (H _ _ _ _ (JMeq_refl x))
     | _ -> _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      specialize (H _ _ _ _ _ (JMeq_refl x))
+      refine_hyp (H _ _ _ _ _ (JMeq_refl x))
     | ?x = _ -> _ =>
-      specialize (H (refl_equal x))
+      refine_hyp (H (refl_equal x))
     | _ -> ?x = _ -> _ =>
-      specialize (H _ (refl_equal x))
+      refine_hyp (H _ (refl_equal x))
     | _ -> _ -> ?x = _ -> _ =>
-      specialize (H _ _ (refl_equal x))
+      refine_hyp (H _ _ (refl_equal x))
     | _ -> _ -> _ -> ?x = _ -> _ =>
-      specialize (H _ _ _ (refl_equal x))
+      refine_hyp (H _ _ _ (refl_equal x))
     | _ -> _ -> _ -> _ -> ?x = _ -> _ =>
-      specialize (H _ _ _ _ (refl_equal x))
+      refine_hyp (H _ _ _ _ (refl_equal x))
     | _ -> _ -> _ -> _ -> _ -> ?x = _ -> _ =>
-      specialize (H _ _ _ _ _ (refl_equal x))
+      refine_hyp (H _ _ _ _ _ (refl_equal x))
   end.
 
 Ltac simpl_IH_eqs H := repeat simpl_IH_eq H.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 9cb7725c0f..5c904e2194 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. *)