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 | |
| parent | 44b5603cae95f9ed42fc29b01ebf5d917da4ecd5 (diff) | |
Fix a name clash
| -rw-r--r-- | src/Reflection/Named/NameUtilProperties.v | 2 | ||||
| -rw-r--r-- | src/Util/ListUtil.v | 10 |
2 files changed, 6 insertions, 6 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))] |- _ ] diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 902d4cb7e..df355d202 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -782,16 +782,16 @@ Lemma skipn_firstn {A} (ls : list A) n m Proof. revert n m; induction ls, m, n; simpl; autorewrite with simpl_skipn simpl_firstn; boring_list. Qed. -Lemma firstn_skipn {A} (ls : list A) n m +Lemma firstn_skipn_add {A} (ls : list A) n m : firstn n (skipn m ls) = skipn m (firstn (m + n) ls). Proof. revert n m; induction ls, m; simpl; autorewrite with simpl_skipn simpl_firstn; boring_list. Qed. -Lemma firstn_skipn' {A} (ls : list A) n m +Lemma firstn_skipn_add' {A} (ls : list A) n m : firstn n (skipn m ls) = skipn m (firstn (n + m) ls). -Proof. rewrite firstn_skipn; do 2 f_equal; auto with arith. Qed. -Hint Rewrite <- @firstn_skipn @firstn_skipn' : simpl_firstn. -Hint Rewrite <- @firstn_skipn @firstn_skipn' : simpl_skipn. +Proof. rewrite firstn_skipn_add; do 2 f_equal; auto with arith. Qed. +Hint Rewrite <- @firstn_skipn_add @firstn_skipn_add' : simpl_firstn. +Hint Rewrite <- @firstn_skipn_add @firstn_skipn_add' : simpl_skipn. Lemma firstn_app_inleft : forall {A} n (xs ys : list A), (n <= length xs)%nat -> firstn n (xs ++ ys) = firstn n xs. |