diff options
| author | Kathy Gray | 2016-02-04 11:53:29 +0000 |
|---|---|---|
| committer | Kathy Gray | 2016-02-04 11:53:29 +0000 |
| commit | ada40991699e649e4e98e09a16bb0ba1b3ff2d74 (patch) | |
| tree | e092c93ff4f5bbd2d0afb894313e9ae2b7c0a01e /src | |
| parent | f3e01108eeb612a168f9ef4beac0b5747eeffbc8 (diff) | |
and for quot_s
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_internal.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index c85faba4..95c9c245 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1999,7 +1999,7 @@ let initial_typ_env = (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")]) (mk_range (mk_nv "q") (mk_nv "r")))), (External (Some "quot_signed")), - [GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "o"),n_one); + [(*GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "o"),n_one);*) LtEq(Specc(Parse_ast.Int("quot",None)),Guarantee,(mk_mult (mk_nv "p") (mk_nv "r")),mk_nv "m")], pure_e,pure_e,nob); Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), |