diff options
| -rw-r--r-- | src/rewrites.ml | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index a61f2622..debce3d1 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -241,8 +241,19 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = | (l, None) -> (l, None) in - rewrite_defs_base { - rewriters_base with rewrite_exp = (fun _ -> map_exp_annot rewrite_annot) + let rewrite_def rewriters = function + | DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), (l, Some (env, typ, eff)))) -> + let typschm = match typschm with + | TypSchm_aux (TypSchm_ts (tq, typ), l) -> + TypSchm_aux (TypSchm_ts (tq, rewrite_typ env typ), l) + in + let a = rewrite_annot (l, Some (env, typ, eff)) in + DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), a)) + | d -> Rewriter.rewrite_def rewriters d + in + + rewrite_defs_base { rewriters_base with + rewrite_exp = (fun _ -> map_exp_annot rewrite_annot); rewrite_def = rewrite_def }, rewrite_typ |