diff options
| -rw-r--r-- | theories/Lists/PolyList.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index 8a5e0421a0..cdc0f36553 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -16,9 +16,12 @@ Section Lists. Variable A : Set. Set Implicit Arguments. +Set Contextual Implicits. Inductive list : Set := nil : list | cons : A -> list -> list. +Unset Contextual Implicits. + (*************************) (** Discrimination *) (*************************) @@ -547,7 +550,6 @@ End Reverse_Induction. End Lists. -Implicits nil [1]. V7only [Implicits nil [].]. Hints Resolve nil_cons app_nil_end ass_app app_ass : datatypes v62. |