From 4a2ef2747950e8a28bfce7ca641bedd7ef71bea1 Mon Sep 17 00:00:00 2001 From: ckeller Date: Wed, 21 Apr 2021 09:46:30 +0200 Subject: 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 . --- src/trace/coqTerms.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/trace/coqTerms.mli') diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli index bf626b3..b5ca6b7 100644 --- a/src/trace/coqTerms.mli +++ b/src/trace/coqTerms.mli @@ -261,3 +261,7 @@ val mk_nat : Structures.constr -> int val mk_N : Structures.constr -> int val mk_Z : Structures.constr -> int val mk_bvsize : Structures.constr -> int + +(* Switches between constr and OCaml *) +val option_of_constr_option : Structures.constr -> Structures.constr option +val list_of_constr_tuple : Structures.constr -> Structures.constr list -- cgit