diff options
Diffstat (limited to 'src/trace/smtForm.mli')
| -rw-r--r-- | src/trace/smtForm.mli | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli index 9678b4c..6a5fca8 100644 --- a/src/trace/smtForm.mli +++ b/src/trace/smtForm.mli @@ -22,7 +22,7 @@ module type ATOM = val is_bool_type : t -> bool val is_bv_type : t -> bool - val to_smt : Format.formatter -> t -> unit + val to_smt : ?debug:bool -> Format.formatter -> t -> unit val logic : t -> logic end @@ -77,7 +77,7 @@ module type FORM = val get : ?declare:bool -> reify -> pform -> t (** Given a coq term, build the corresponding formula *) - val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t + val of_coq : (CoqInterface.constr -> hatom) -> reify -> CoqInterface.constr -> t val hash_hform : (hatom -> hatom) -> reify -> t -> t @@ -90,20 +90,20 @@ module type FORM = (** Producing Coq terms *) - val to_coq : t -> Structures.constr + val to_coq : t -> CoqInterface.constr val pform_tbl : reify -> pform array val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array - val interp_tbl : reify -> Structures.constr * Structures.constr + val interp_tbl : reify -> CoqInterface.constr * CoqInterface.constr val nvars : reify -> int - (** Producing a Coq term corresponding to the interpretation - of a formula *) - (** [interp_atom] map [hatom] to coq term, it is better if it produce - shared terms. *) + (* Producing a Coq term corresponding to the interpretation + of a formula *) + (* [interp_atom] map [hatom] to coq term, it is better if it produce + shared terms. *) val interp_to_coq : - (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t -> - t -> Structures.constr + (hatom -> CoqInterface.constr) -> (int, CoqInterface.constr) Hashtbl.t -> + t -> CoqInterface.constr (* Unstratified terms *) type atom_form_lit = |