Module Theory.Sym

module Sym: sig .. end
Dynamically typed morphisms

type pack = {
   ar : Term.constr;
   value : Term.constr;
   morph : Term.constr;
}
mimics the Coq record Sym.pack
val typ : Term.constr lazy_t
val mk_pack : Coq.Relation.t -> pack -> Term.constr
mk_pack rlt (ar,value,morph)
val null : Coq.Relation.t -> Term.constr
null builds a dummy (identity) symbol, given an Coq.Relation.t