diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-10-24 17:28:51 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-10-24 17:28:51 +0200 |
| commit | 7e38b6627caaab7d19c4fc0ee542a67d9f8970c2 (patch) | |
| tree | 375ed6a0a45131e479dea6d3d8c9cf64a786fcf7 /theories/Lists | |
| parent | 46462c3cc69e97bf3260f1aad5faaa6eaf6c2722 (diff) | |
Remove v62 from stdlib.
This old compatibility hint database can be safely removed
now that coq-contribs do not depend on it anymore.
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 16 | ||||
| -rw-r--r-- | theories/Lists/Streams.v | 2 |
2 files changed, 9 insertions, 9 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index bf21ffb47..30f1dec22 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -340,11 +340,11 @@ Section Facts. End Facts. -Hint Resolve app_assoc app_assoc_reverse: datatypes v62. -Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62. -Hint Immediate app_eq_nil: datatypes v62. -Hint Resolve app_eq_unit app_inj_tail: datatypes v62. -Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62. +Hint Resolve app_assoc app_assoc_reverse: datatypes. +Hint Resolve app_comm_cons app_cons_not_nil: datatypes. +Hint Immediate app_eq_nil: datatypes. +Hint Resolve app_eq_unit app_inj_tail: datatypes. +Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes. @@ -1544,7 +1544,7 @@ Section length_order. End length_order. Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: - datatypes v62. + datatypes. (******************************) @@ -1613,7 +1613,7 @@ Section SetIncl. End SetIncl. Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons - incl_app: datatypes v62. + incl_app: datatypes. (**************************************) @@ -2365,7 +2365,7 @@ Notation rev_acc := rev_append (only parsing). Notation rev_acc_rev := rev_append_rev (only parsing). Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) -Hint Resolve app_nil_end : datatypes v62. +Hint Resolve app_nil_end : datatypes. (* end hide *) Section Repeat. diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 7ec3d2503..1c302b22f 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -51,7 +51,7 @@ Lemma tl_nth_tl : Proof. simple induction n; simpl; auto. Qed. -Hint Resolve tl_nth_tl: datatypes v62. +Hint Resolve tl_nth_tl: datatypes. Lemma Str_nth_tl_plus : forall (n m:nat) (s:Stream), |