diff options
| author | Brian Campbell | 2019-01-09 13:43:16 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-01-09 13:43:16 +0000 |
| commit | 1c80d84c47faef38149e87e000c6721f6aa6245e (patch) | |
| tree | fb622ec7041c00eb021f7bd65f0d40b47a1c7c56 /src | |
| parent | 7d33d9c1837149d31df06b803ed4dbf2ce4053ca (diff) | |
Coq: the division used in smt.sail should be Euclidean
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 5cf17056..20db317b 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -239,9 +239,9 @@ let doc_nexp ctx ?(skip_vars=KidSet.empty) nexp = and app (Nexp_aux (n,l) as nexp) = match n with | Nexp_app (Id_aux (Id "div",_), [n1;n2]) - -> separate space [string "Z.quot"; atomic n1; atomic n2] + -> separate space [string "ZEuclid.div"; atomic n1; atomic n2] | Nexp_app (Id_aux (Id "mod",_), [n1;n2]) - -> separate space [string "Z.rem"; atomic n1; atomic n2] + -> separate space [string "ZEuclid.modulo"; atomic n1; atomic n2] | Nexp_app (Id_aux (Id "abs_atom",_), [n1]) -> separate space [string "Z.abs"; atomic n1] | _ -> atomic nexp |