diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 15:39:35 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-27 15:39:35 +0200 |
| commit | 0334ceccaf14716d81db8a73f7d414d33b91cd8b (patch) | |
| tree | 9880cfed3e65f2cc6eb7c063ee52c339f0412ed7 /src/trace | |
| parent | db9bb4f7ba88c938e882f9a30c6456d73b793491 (diff) | |
| download | smtcoq-0334ceccaf14716d81db8a73f7d414d33b91cd8b.tar.gz smtcoq-0334ceccaf14716d81db8a73f7d414d33b91cd8b.zip | |
Zeq_bool -> Z.eqb
Diffstat (limited to 'src/trace')
| -rw-r--r-- | src/trace/coqTerms.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 6c76f9d..1874d5f 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -52,10 +52,7 @@ let cltb = gen_constant z_modules "ltb" let cleb = gen_constant z_modules "leb" let cgeb = gen_constant z_modules "geb" let cgtb = gen_constant z_modules "gtb" -(* Je ne comprends pas pourquoi ça fonctionne avec Zeq_bool et pas avec - Z.eqb *) -(* let ceqbZ = gen_constant z_modules "eqb" *) -let ceqbZ = gen_constant [["Coq";"ZArith";"Zbool"]] "Zeq_bool" +let ceqbZ = gen_constant z_modules "eqb" (* Booleans *) let bool_modules = [["Coq";"Bool";"Bool"]] |