helm/EXPORT/exportcoq/provacoqcontribRing.v

   1 Require Export Xml.
   2
   3 Require ArithRing.
   4 Require Quote.
   5 Require Ring.
   6 Require Ring_abstract.
   7 Require Ring_normalize.
   8 Require Ring_theory.
   9 Require ZArithRing.
  10
  11 Print XML Module Disk "examples" ArithRing.
  12 Print XML Module Disk "examples" Quote.
  13 Print XML Module Disk "examples" Ring.
  14 Print XML Module Disk "examples" Ring_abstract.
  15 Print XML Module Disk "examples" Ring_normalize.
  16 Print XML Module Disk "examples" Ring_theory.
  17 Print XML Module Disk "examples" ZArithRing.