blob: f0e5d71811321124d4b93133958a091231c31f16 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(* See discussion in #668 for whether manual implicit arguments should
be allowed in notations or not *)
Set Warnings "+syntax".
Fail Notation D1 := (forall {T : Type} ( x : T ) , Type).
Definition DD1 ( A : forall {T : Type} (x : T), Type ) := A 1.
Fail Definition DD1' ( A : D1 ) := A 1. (* Toplevel input, characters 32-33:
Error: In environment
A : forall T : Type, T -> Type
The term "1" has type "nat" while it is expected to have type
"Type".
*)
|
