functor (T : Nunchaku_core.TermTyped.S) ->
  sig
    type term = T.t
    type env
    val empty_env : TypeInference.Convert.env
    val convert_ty :
      env:TypeInference.Convert.env ->
      Nunchaku_core.UntypedAST.ty ->
      TypeInference.Convert.term TypeInference.or_error
    val convert_ty_exn :
      env:TypeInference.Convert.env ->
      Nunchaku_core.UntypedAST.ty -> TypeInference.Convert.term
    val convert_term :
      env:TypeInference.Convert.env ->
      Nunchaku_core.UntypedAST.term ->
      TypeInference.Convert.term TypeInference.or_error
    val convert_term_exn :
      env:TypeInference.Convert.env ->
      Nunchaku_core.UntypedAST.term -> TypeInference.Convert.term
    val generalize :
      close:[ `Forall | `Fun | `NoClose ] ->
      TypeInference.Convert.term ->
      TypeInference.Convert.term *
      TypeInference.Convert.term TypeInference.var list
    type statement =
        (TypeInference.Convert.term, TypeInference.Convert.term)
        Nunchaku_core.Statement.t
    val convert_statement :
      env:TypeInference.Convert.env ->
      Nunchaku_core.UntypedAST.statement ->
      (TypeInference.Convert.statement * TypeInference.Convert.env)
      TypeInference.or_error
    val convert_statement_exn :
      env:TypeInference.Convert.env ->
      Nunchaku_core.UntypedAST.statement ->
      TypeInference.Convert.statement * TypeInference.Convert.env
    type problem =
        (TypeInference.Convert.term, TypeInference.Convert.term)
        Nunchaku_core.Problem.t
    val convert_problem :
      env:TypeInference.Convert.env ->
      Nunchaku_core.UntypedAST.statement CCVector.ro_vector ->
      (TypeInference.Convert.problem * TypeInference.Convert.env)
      TypeInference.or_error
    val convert_problem_exn :
      env:TypeInference.Convert.env ->
      Nunchaku_core.UntypedAST.statement CCVector.ro_vector ->
      TypeInference.Convert.problem * TypeInference.Convert.env
  end