aboutsummaryrefslogtreecommitdiffstats
path: root/src/verit/verit.mli
diff options
context:
space:
mode:
authorckeller <ckeller@users.noreply.github.com>2021-04-21 09:46:30 +0200
committerGitHub <noreply@github.com>2021-04-21 09:46:30 +0200
commit4a2ef2747950e8a28bfce7ca641bedd7ef71bea1 (patch)
tree3ceff26534e6f4116969b143725700077993ec6f /src/verit/verit.mli
parent1c5ff0e9d329518158fd39fe9875e8f197bdb8f6 (diff)
downloadsmtcoq-4a2ef2747950e8a28bfce7ca641bedd7ef71bea1.tar.gz
smtcoq-4a2ef2747950e8a28bfce7ca641bedd7ef71bea1.zip
Convert hypotheses from Prop to bool (#89)
* This PR converts hypotheses given to the tactics verit, verit_no_check, smt and smt_no_check from Prop to bool when needed. * Some current limitations are detailed in src/PropToBool.v. * Partially enhances #30 .
Diffstat (limited to 'src/verit/verit.mli')
-rw-r--r--src/verit/verit.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 6fa62d8..4b84b58 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -19,5 +19,5 @@ val parse_certif :
val checker : string -> string -> unit
val checker_debug : string -> string -> unit
val theorem : Structures.id -> string -> string -> unit
-val tactic : Structures.constr list -> Structures.constr_expr list -> Structures.tactic
-val tactic_no_check : Structures.constr list -> Structures.constr_expr list -> Structures.tactic
+val tactic : EConstr.t -> Structures.constr_expr list -> Structures.tactic
+val tactic_no_check : EConstr.t -> Structures.constr_expr list -> Structures.tactic