Main.v

Require General.

Section PTS_modulaire.

  Variable sort: Set.
  Hypothesis eq_sort_dec: (s,s':sort)(decide s=s').

  Load Ltermes.
  Load Ltyping.
  Load Lrules.
  Load Lcumul.
  Load Llambda.

End PTS_modulaire.

23/12/98, 14:30