aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Case11.v
blob: 445ffac8cbf50bc9ce264398894d9718048f3ce4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
(* L'algo d'inférence du prédicat doit gérer le K-rédex dans le type de b *)
(* Problème rapporté par Solange Coupet *)

Section A.

Variables (Alpha : Set) (Beta : Set).

Definition nodep_prod_of_dep (c : sigS (fun a : Alpha => Beta)) :
  Alpha * Beta := match c with
                  | existS _ a b => (a, b)
                  end.

End A.