diff options
Diffstat (limited to 'test-suite/output/notation_principal_scope.v')
| -rw-r--r-- | test-suite/output/notation_principal_scope.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/output/notation_principal_scope.v b/test-suite/output/notation_principal_scope.v new file mode 100644 index 0000000000..6bd911501d --- /dev/null +++ b/test-suite/output/notation_principal_scope.v @@ -0,0 +1,23 @@ +Arguments conj {_ _} _ _%function. + +Set Warnings "+inconsistent-scopes". +Fail Notation pp X := (conj X X). + +Fail Notation pp := 1 (only printing). + +Fail Notation pp X := nonexisting. + +Fail Notation pp X := (conj X X) (X, X in scope nat_scope). + +Notation pp X := (conj X X) (X in scope nat_scope). + +Notation "$" := I (only parsing) : nat_scope. +Notation "$" := (I I) (only parsing) : bool_scope. + +Open Scope bool_scope. +Check pp $. +Fail Check pp (id $). + +Notation pp1 X := (X%nat) (X in scope bool_scope). +Notation pp2 X := ((X + X)%type) (X in scope bool_scope). +Notation pp3 X := (((X, X)%type, X)%nat) (X in scope bool_scope). |