diff options
Diffstat (limited to 'src/jib/jib_smt.mli')
| -rw-r--r-- | src/jib/jib_smt.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli index 421cbf2c..820f06d1 100644 --- a/src/jib/jib_smt.mli +++ b/src/jib/jib_smt.mli @@ -92,7 +92,7 @@ type ctx = { generating the SMT for. Used for error messages. *) arg_stack : (int * string) Stack.t; (** Used internally to keep track of function argument names *) - ast : Type_check.tannot defs; + ast : Type_check.tannot ast; (** The fully type-checked ast *) shared : ctyp Bindings.t; (** Shared variables. These variables do not get renamed by @@ -124,7 +124,7 @@ type ctx = { } (** Compile an AST into Jib suitable for SMT generation, and initialise a context. *) -val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * Jib_compile.ctx * ctx +val compile : Type_check.Env.t -> Type_check.tannot ast -> cdef list * Jib_compile.ctx * ctx (* TODO: Currently we internally use mutable stacks and queues to avoid any issues with stack overflows caused by some non @@ -154,7 +154,7 @@ module Make_optimizer(S : Sequence) : sig end val serialize_smt_model : - string -> Type_check.Env.t -> Type_check.tannot defs -> unit + string -> Type_check.Env.t -> Type_check.tannot ast -> unit val deserialize_smt_model : string -> cdef list * ctx @@ -165,5 +165,5 @@ val generate_smt : (string * string * l * 'a val_spec) Bindings.t (* See Property.find_properties *) -> (string -> string) (* Applied to each function name to generate the file name for the smtlib file *) -> Type_check.Env.t - -> Type_check.tannot defs + -> Type_check.tannot ast -> unit |