diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-21 10:00:58 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-21 10:00:58 +0200 |
| commit | 13d2c8be2ffb84bc8d40064b223562832e5a5a7e (patch) | |
| tree | 8e9b4c8b8c31ee95bcd7eeffaacf72b40215adb3 /src/trace/coqTerms.mli | |
| parent | 0955c9b404b2bebbe76a15daaad09c03670e849e (diff) | |
| parent | 4a2ef2747950e8a28bfce7ca641bedd7ef71bea1 (diff) | |
| download | smtcoq-13d2c8be2ffb84bc8d40064b223562832e5a5a7e.tar.gz smtcoq-13d2c8be2ffb84bc8d40064b223562832e5a5a7e.zip | |
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10
Diffstat (limited to 'src/trace/coqTerms.mli')
| -rw-r--r-- | src/trace/coqTerms.mli | 4 |
1 files changed, 4 insertions, 0 deletions
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 |