helm/EXPORT/exportcoq/provacoqLogic.v

   1 Require Export Xml.
   2
   3 Require Classical.
   4 Require Classical_Pred_Set.
   5 Require Classical_Pred_Type.
   6 Require Classical_Prop.
   7 Require Classical_Type.
   8 Require Eqdep.
   9 Require Eqdep_dec.
  10
  11 Print XML Module Disk "examples" Classical.
  12 Print XML Module Disk "examples" Classical_Pred_Set.
  13 Print XML Module Disk "examples" Classical_Pred_Type.
  14 Print XML Module Disk "examples" Classical_Prop.
  15 Print XML Module Disk "examples" Classical_Type.
  16 Print XML Module Disk "examples" Eqdep.
  17 Print XML Module Disk "examples" Eqdep_dec.