diff options
| -rw-r--r-- | theories/Lists/PolyList.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index 5baa768917..8a5e0421a0 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -211,8 +211,7 @@ Proof. Qed. End length_order. -Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons -. +Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons. (*********************************) (** The [In] predicate *) @@ -548,6 +547,9 @@ End Reverse_Induction. End Lists. +Implicits nil [1]. +V7only [Implicits nil [].]. + Hints Resolve nil_cons app_nil_end ass_app app_ass : datatypes v62. Hints Resolve app_comm_cons app_cons_not_nil : datatypes v62. Hints Immediate app_eq_nil : datatypes v62. @@ -568,7 +570,7 @@ Section Map. Variables A,B:Set. Variable f:A->B. Fixpoint map [l:(list A)] : (list B) := - Cases l of + Cases l of nil => (nil B) | (cons a t) => (cons (f a) (map t)) end. @@ -681,5 +683,3 @@ Reflexivity. Qed. End Functions_on_lists. - -Unset Implicit Arguments. |