summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4017.v
blob: aa810f4f0e86ef548e909d12f9cb82cfd6745854 (plain)
1
2
3
4
5
6
7
8
Set Implicit Arguments.

(* Use of implicit arguments was lost in multiple variable declarations *)
Variables 
  (A1 : Type)
  (A2 : forall (x1 : A1), Type) 
  (A3 : forall (x1 : A1) (x2 : A2 x1), Type)
  (A4 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2), Type).