diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewrites.ml | 1 | ||||
| -rw-r--r-- | src/type_check.ml | 2 |
2 files changed, 1 insertions, 2 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index ea8ccaf9..8df5ce02 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5108,7 +5108,6 @@ let rewrite_defs_c = [ ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); - ("guarded_pats", rewrite_defs_guarded_pats); ("exp_lift_assign", rewrite_defs_exp_lift_assign); ("constraint", rewrite_constraint); ("trivial_sizeof", rewrite_trivial_sizeof); diff --git a/src/type_check.ml b/src/type_check.ml index cb20ae2e..4d8c3bcf 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -4327,7 +4327,7 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md typ_debug (lazy ("Checking mapdef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ))); let vs_def, env = if not have_val_spec then - [mk_val_spec env quant typ id], Env.add_val_spec id (quant, typ) env + [mk_val_spec env quant (Env.expand_synonyms env typ) id], Env.add_val_spec id (quant, typ) env else [], env in |