diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:59:39 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:59:39 +0200 |
| commit | 220afeb0eb1b0b63fccd29e254f3179cac834c12 (patch) | |
| tree | 7ff6cc51b5e09034658fe053ccff4675a964ed13 /src/trace/smtAtom.mli | |
| parent | a827528c0435f2006560b8cb359420bbffe85881 (diff) | |
| parent | 4c348a170ea80d20f08ccd5b20e98f56b9267485 (diff) | |
| download | smtcoq-220afeb0eb1b0b63fccd29e254f3179cac834c12.tar.gz smtcoq-220afeb0eb1b0b63fccd29e254f3179cac834c12.zip | |
Merge branch 'coq-8.12' of github.com:smtcoq/smtcoq into coq-8.13
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 |