object
  method virtual basename : string -> string
  method datatype : Lang.adt -> string
  method datatypename : string -> string
  method field : Lang.field -> string
  method fieldname : string -> string
  method funname : string -> string
  method virtual infoprover : 'Lang.infoprover -> 'a
  method link : Lang.lfun -> Qed.Engine.link
end