diff options
| author | Alasdair Armstrong | 2017-07-28 15:50:08 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-07-28 15:50:08 +0100 |
| commit | 21f45448b9bd5d2653481d6911659b35da5dd5d3 (patch) | |
| tree | 605465523a567082f2931cbfc9d430112dd9e642 /src | |
| parent | 3386adef7cd297279b22b2fbb4f3f7399c54a8c2 (diff) | |
Mips TLB existential example
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index b4460992..fea94a90 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2514,7 +2514,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = let nc_true = nc_eq (nconstant 0) (nconstant 0) in let typ_ret = - if existentials = [] + if KidSet.is_empty (KidSet.inter (typ_frees typ_ret) (KidSet.of_list existentials)) then typ_ret else mk_typ (Typ_exist (existentials, List.fold_left nc_and nc_true ex_constraints, typ_ret)) in |