diff options
| author | Jon French | 2018-05-16 15:44:19 +0100 |
|---|---|---|
| committer | Jon French | 2018-05-16 15:44:19 +0100 |
| commit | a7563156f1ea9ca71c2d4cd0de4bad67f0f99b30 (patch) | |
| tree | 882c978f6e50369e8ddb0f4871755e9f33b4a715 /src/rewrites.ml | |
| parent | e2d8fe4d847b6e8f71eecd7aa6d15799bd2a2e11 (diff) | |
Add support for inline val-spec declaration for mappings
This means that a mapping which formerly had to be pre-declared like
val name : a <-> b
...
mapping name {
x <-> y,
...
}
can now be shortened to
mapping name : a <-> b {
x <-> y,
...
}
Diffstat (limited to 'src/rewrites.ml')
| -rw-r--r-- | src/rewrites.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index e41318dd..58ff885f 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -3758,7 +3758,7 @@ let rewrite_defs_realise_mappings (Defs defs) = | MPat_aux (MPat_when (mpat2, _), _)-> realise_mpexps true (append_placeholder mpexp) (mk_mpexp (MPat_pat (mk_mpat (MP_app ((mk_id "Some"), [ mk_mpat (MP_tup [mpat2; strlen]) ]))))) in - let realise_mapdef (MD_aux (MD_mapping (id, mapcls), ((l, (tannot:tannot)) as annot))) = + let realise_mapdef (MD_aux (MD_mapping (id, _, mapcls), ((l, (tannot:tannot)) as annot))) = let forwards_id = mk_id (string_of_id id ^ "_forwards") in let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in let backwards_id = mk_id (string_of_id id ^ "_backwards") in |