(module dracula (file "require-provide-language.scm")
  
  (require (all-except "dracula-core.scm"
                       require
                       #%module-begin
                       #%app
                       #%top))
  (provide (all-from "dracula-core.scm"))

  (require "defstructure.scm") (provide (all-from "defstructure.scm"))
  (require "deflist.scm") (provide (all-from "deflist.scm"))
  
  (require (file "primitive-procedures/acl2-prims.scm")) 
  (provide (all-from (file "primitive-procedures/acl2-prims.scm")))
  
  (require "dracula-module-begin.scm")
  (provide (rename dracula-module-begin #%module-begin)
           (rename dracula-module-begin #%plain-module-begin))
  (require (only mzscheme #%top-interaction)) (provide #%top-interaction)
  (require "acl2-top.scm" "acl2-app.scm") (provide (rename acl2-top #%top) (rename acl2-app #%app))
  
  #|
  (require (lib "docprovide.ss" "syntax")
           (only mzscheme read-case-sensitive))
  
  (require (all-except (file "acl2-language.scm") 
                       provide 
                       require 
                       require-for-syntax display #%module-begin
                       collect-garbage expand)
           (file "private/acl2-module-begin.scm")
           (file "private/forms/acl2-app.scm")
           (file "private/modules/provide-contract.scm"))
  
  (provide (all-from-except (file "acl2-language.scm") 
                            #%app
                            defmacro)
           #%app
           (rename acl2-module-begin #%module-begin)
           (rename acl2-provide/contract provide/c)
           provide-definition)
  
  (require (file "private/modules/acl2-require.scm"))
  (provide (rename acl2-require require))
  
  (require "private/modules/acl2-any.scm")
  (provide anyp)
  
  (require "private/forms/with-prover-time-limit.scm") (provide with-prover-time-limit)
  
  ;; (require (lib "contract.ss")) (provide (all-from (lib "contract.ss")))
|#
  )