diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1951.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1951.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1951.v b/test-suite/bugs/closed/shouldsucceed/1951.v index 4fbd6b22d..12c0ef9bf 100644 --- a/test-suite/bugs/closed/shouldsucceed/1951.v +++ b/test-suite/bugs/closed/shouldsucceed/1951.v @@ -28,7 +28,7 @@ Inductive sg : Type := Sg. (* single *) Definition ipl2 (P : a -> Type) := (* in Prop, that means P is true forall *) fold_right (fun x => prod (P x)) sg. (* the elements of a given list *) -Definition ind +Definition ind : forall S : a -> Type, (forall ls : list a, ipl2 S ls -> S (b ls)) -> forall s : a, S s := fun (S : a -> Type) |