blob: fd5d139c6b0ab2851061874fd80d47ea5a853834 (
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.
|
