diff options
| author | Alasdair Armstrong | 2018-01-12 17:27:37 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-01-12 17:27:37 +0000 |
| commit | e56eafdb87f3f4e362cca7d0a6ca3d8a0e849b44 (patch) | |
| tree | 4b19d06dd6a234c5524c88e8aeceefce41ca8864 /src/monomorphise.ml | |
| parent | ebc33211b0a3a6c14bbe4106b9a618b8ac594f52 (diff) | |
| parent | ffcf8a814cdd23eaff9286835478afb66fbb0029 (diff) | |
Merge remote-tracking branch 'origin/experiments' into sail2
Diffstat (limited to 'src/monomorphise.ml')
| -rw-r--r-- | src/monomorphise.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index af3484ec..06f0683a 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -102,7 +102,7 @@ let rec subst_nc substs (NC_aux (nc,l) as n_constraint) = begin match KBindings.find kid substs with | Nexp_aux (Nexp_constant i,_) -> - if List.mem i is then re NC_true else re NC_false + if List.exists (fun j -> Big_int.equal i j) is then re NC_true else re NC_false | nexp -> raise (Reporting_basic.err_general l ("Unable to substitute " ^ string_of_nexp nexp ^ @@ -1691,11 +1691,10 @@ let rewrite_size_parameters env (Defs defs) = let sizes_funcl fsizes (FCL_aux (FCL_Funcl (id,pexp),(l,_))) = let sizes = size_vars pexp in let pat,guard,exp,pannot = destruct_pexp pexp in - (* TODO: what, if anything, should sequential be? *) let visible_tyvars = KidSet.union - (Pretty_print_lem.lem_tyvars_of_typ false true (pat_typ_of pat)) - (Pretty_print_lem.lem_tyvars_of_typ false true (typ_of exp)) + (Pretty_print_lem.lem_tyvars_of_typ (pat_typ_of pat)) + (Pretty_print_lem.lem_tyvars_of_typ (typ_of exp)) in let expose_tyvars = KidSet.diff sizes visible_tyvars in let parameters = match pat with |