Module Elaboration.ElaborateSource

module E = Parsers.Entry
Sourcemodule L = Common.Log
Sourcemodule M = Api.Meta
module R = Kernel.Rule
module T = Kernel.Term
Sourcetype t = {
  1. file : F.cout F.t;
    (*

    File where universe declarations are printed

    *)
  2. meta : M.cfg;
    (*

    Meta rules that translates universes to the pre-universe variable

    *)
}
Sourceval mk_term : t -> T.term -> T.term

mk_term env t replaces all the concrete universes in t by a fresh variable using the environment env.

Sourceval mk_rule : t -> 'a R.rule -> 'a R.rule

mkrule env r replaces all the concrete universes in rule.rhs by a fresh variable using the environement env.

Sourceval mk_entry : t -> E.entry -> E.entry

mk_entry env entry replaces all the concrete universes in entry by a fresh variable using the environment env. Commands are skipped.