aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2667.v
blob: 0631e5358dde54bd75192333aa7d4f90fb4ad8a6 (plain)
1
2
3
4
5
6
7
8
9
10
11
(* Check that extra arguments to Arguments Scope do not disturb use of *)
(* scopes in constructors *)

Inductive stmt : Type := Sskip: stmt | Scall : nat -> stmt.
Bind Scope Cminor with stmt.

(* extra argument is ok because of possible coercion to funclass *)
Arguments Scope Scall [_ Cminor ].

(* extra argument is ok because of possible coercion to funclass *)
Fixpoint f (c: stmt) : Prop := match c with Scall _ => False | _ => False end.