diff options
| author | vblot <24938579+vblot@users.noreply.github.com> | 2021-05-28 18:29:37 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-28 18:29:37 +0200 |
| commit | e12110637730d067c216abcc86185b761189b342 (patch) | |
| tree | c9ed415bbdadb2801e4917aae4a803035b13d4e8 /src/trace/smtAtom.mli | |
| parent | 52980aab9541a12619eb9191a94e9b2ba4684447 (diff) | |
| download | smtcoq-e12110637730d067c216abcc86185b761189b342.tar.gz smtcoq-e12110637730d067c216abcc86185b761189b342.zip | |
getting rid of native-coq (#95)
Diffstat (limited to 'src/trace/smtAtom.mli')
| -rw-r--r-- | src/trace/smtAtom.mli | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index 645a638..27737ff 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -76,14 +76,14 @@ module Op : val create : unit -> reify_tbl - val declare : reify_tbl -> Structures.constr -> btype array -> + val declare : reify_tbl -> CoqInterface.constr -> btype array -> btype -> string option -> indexed_op - val of_coq : reify_tbl -> Structures.constr -> indexed_op + val of_coq : reify_tbl -> CoqInterface.constr -> indexed_op - val interp_tbl : Structures.constr -> - (btype array -> btype -> Structures.constr -> Structures.constr) -> - reify_tbl -> Structures.constr + val interp_tbl : CoqInterface.constr -> + (btype array -> btype -> CoqInterface.constr -> CoqInterface.constr) -> + reify_tbl -> CoqInterface.constr val to_list : reify_tbl -> (int * (btype array) * btype * indexed_op) list @@ -142,18 +142,18 @@ module Atom : (** Given a coq term, build the corresponding atom *) exception UnknownUnderForall val of_coq : ?eqsym:bool -> SmtBtype.reify_tbl -> Op.reify_tbl -> - reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t + reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> CoqInterface.constr -> t - val get_coq_term_op : int -> Structures.constr + val get_coq_term_op : int -> CoqInterface.constr - val to_coq : t -> Structures.constr + val to_coq : t -> CoqInterface.constr val to_array : reify_tbl -> 'a -> (atom -> 'a) -> 'a array - val interp_tbl : reify_tbl -> Structures.constr + val interp_tbl : reify_tbl -> CoqInterface.constr - val interp_to_coq : Structures.constr -> (int, Structures.constr) Hashtbl.t -> - t -> Structures.constr + val interp_to_coq : CoqInterface.constr -> (int, CoqInterface.constr) Hashtbl.t -> + t -> CoqInterface.constr val logic : t -> SmtMisc.logic @@ -201,5 +201,5 @@ module Trace : sig end -val make_t_i : SmtBtype.reify_tbl -> Structures.constr -val make_t_func : Op.reify_tbl -> Structures.constr -> Structures.constr +val make_t_i : SmtBtype.reify_tbl -> CoqInterface.constr +val make_t_func : Op.reify_tbl -> CoqInterface.constr -> CoqInterface.constr |