diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Arguments.v | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations.v | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index bd9240476f..b67ac4f0df 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -10,6 +10,8 @@ Arguments Nat.sub !n !m. About Nat.sub. Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := fun x => (f (fst x), g (snd x)). +Declare Scope foo_scope. +Declare Scope bar_scope. Delimit Scope foo_scope with F. Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never. About pf. diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index fe6c05c39e..adab324cf0 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -76,6 +76,7 @@ Open Scope nat_scope. Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat). Coercion Zpos: nat >-> znat. +Declare Scope znat_scope. Delimit Scope znat_scope with znat. Open Scope znat_scope. |