Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
module type S = Tff_intf.S
(* Typechecking functor *)(* ************************************************************************ *)
module Make (Tag: Dolmen.Intf.Tag.S) (Ty: Dolmen.Intf.Ty.Tff with type 'a tag := 'a Tag.t and type path := Dolmen.Std.Path.t) (T: Dolmen.Intf.Term.Tff with type ty := Ty.t and type ty_var := Ty.Var.t and type ty_const := Ty.Const.t and type ty_def := Ty.def and type 'a tag := 'a Tag.t and type path := Dolmen.Std.Path.t)= struct
include Thf.Make(Tag) (struct include Ty let arrow _ _ = assert false let pi _ _ = assert false end) (struct include T let apply _ _ _ = assert false end)
let empty_env ?st ?expect ?var_infer ?sym_infer ?(order=First_order) ?poly ?poly_args ?quants ?free_wildcards ~warnings ~file builtin_symbols = let env = empty_env ?st ?expect ?var_infer ?sym_infer ~order ?poly ?poly_args ?quants ?free_wildcards ~warnings ~file builtin_symbols in match order with | First_order -> env | Higher_order -> _error env (Located Dolmen.Std.Loc.no_loc) Higher_order_env_in_tff_typechecker
end