ocaml 3.09 transition

[helm.git] / helm / EXPORT / exportprove / prove / provastruct3.v

Section a.
 Section a1.
  Variable A : Prop.
  Variable B : Prop.
  Inductive t1 : Set := k1 : A -> t1.
 End a1.
 
 Inductive t2 [B:Set] : Set := k2 : (t2 B).

 Variable A : Prop.
End a.