diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/implicit.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index b286538316..e8019a908f 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -120,3 +120,7 @@ Check C2 eq_refl. Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop := | C3 : I3 a (n:=0). + +(* Check global implicit declaration over ref not in section *) + +Section D. Global Arguments eq [A] _ _. End D. |