summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorThomas Bauereiss2019-01-31 13:41:03 +0000
committerThomas Bauereiss2019-01-31 13:41:03 +0000
commit3d375ec372aa25405beaddbef68a5eeeffcc66a2 (patch)
treeede14588bb22f87b50b16dba77764bb68d67345f /src
parentb3b3c6c37566459f9b185b7e7ef608423a3ed973 (diff)
Further restrict attention to Int kids
Diffstat (limited to 'src')
-rw-r--r--src/monomorphise.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index ceb8d85a..e16431b8 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -4150,7 +4150,7 @@ let add_bitvector_casts (Defs defs) =
let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),fcl_ann)) =
let fcl_env = env_of_annot fcl_ann in
let (tq,typ) = Env.get_val_spec_orig id fcl_env in
- let quant_kids = List.map kopt_kid (quant_kopts tq) in
+ let quant_kids = List.map kopt_kid (List.filter is_nat_kopt (quant_kopts tq)) in
let ret_typ =
match typ with
| Typ_aux (Typ_fn (_,ret,_),_) -> ret