diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-14 22:33:44 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-14 22:33:44 -0400 |
| commit | 2c2ac41de0bedabc3b8fd53d28f8b65859eb4287 (patch) | |
| tree | f216a5e289d810a29bc7fc22c489d1abafd3277e /src/Reflection/Named | |
| parent | 44b5603cae95f9ed42fc29b01ebf5d917da4ecd5 (diff) | |
Fix a name clash
Diffstat (limited to 'src/Reflection/Named')
| -rw-r--r-- | src/Reflection/Named/NameUtilProperties.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Named/NameUtilProperties.v b/src/Reflection/Named/NameUtilProperties.v index 9f6734eb3..d0ef26b1d 100644 --- a/src/Reflection/Named/NameUtilProperties.v +++ b/src/Reflection/Named/NameUtilProperties.v @@ -35,7 +35,7 @@ Section language. | match goal with | [ H : forall ls, snd (split_mnames _ _ _) = _, H' : context[snd (split_mnames _ _ _)] |- _ ] => rewrite H in H' - | [ H : _ |- _ ] => first [ rewrite <- firstn_skipn in H ] + | [ H : _ |- _ ] => first [ rewrite <- firstn_skipn_add in H ] | [ H : forall ls', fst (split_mnames _ _ _) = _, H' : context[fst (split_mnames _ _ (skipn ?n ?ls))] |- _ ] => rewrite (H (skipn n ls)) in H' | [ H : forall ls', fst (split_mnames _ _ _) = _, H' : context[fst (split_mnames _ ?t (firstn (count_pairs ?t + ?n) ?ls))] |- _ ] |