diff options
| author | Brian Campbell | 2018-04-09 16:05:39 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-04-09 16:05:59 +0100 |
| commit | 91d9047b1cccff67a3130fc5e48dd8eadfe3bb9d (patch) | |
| tree | f779b7ee50844129e314fe1c0ed03d43e2779cab /src | |
| parent | 86402c298c24e47ae49de7fb9748f0a67aaa98d2 (diff) | |
Remove unnecessary restriction on complex nexp rewriting
Diffstat (limited to 'src')
| -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 08feccbe..c88a025e 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3941,10 +3941,9 @@ let rewrite_toplevel_nexps (Defs defs) = else nexp_map, snd (replace_nexp_in_typ env typ' nexp new_nexp) in let rewrite_valspec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (tqs,typ),ts_l),id,ext_opt,is_cast),ann)) = - match tqs, ext_opt "lem" with (* does it really matter if this is wrong? *) - | _, Some _ - | TypQ_aux (TypQ_no_forall,_), _ -> None - | TypQ_aux (TypQ_tq qs, tq_l), None -> + match tqs with + | TypQ_aux (TypQ_no_forall,_) -> None + | TypQ_aux (TypQ_tq qs, tq_l) -> let env = env_of_annot ann in let env = add_typquant tqs env in let nexp_map, typ = rewrite_typ_in_spec env [] typ in |