diff options
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"]] |