diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-09 08:55:34 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-09 08:55:34 +0000 |
| commit | 85972057e714da016b9299f47b833aec31220403 (patch) | |
| tree | 9e28b119cd0457b2990cf549ab64e857bd4e3038 /theories/Program/Equality.v | |
| parent | bd7f800d5fc48dcb7bfae475e796f6e18901fbcb (diff) | |
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
Diffstat (limited to 'theories/Program/Equality.v')
| -rw-r--r-- | theories/Program/Equality.v | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 3e0e8ca2b..11f710997 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. |