diff options
| author | Christopher Pulte | 2016-10-27 00:06:19 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-10-27 00:06:19 +0100 |
| commit | 5cbc35eb6d253e87185bbf247aa1e3db12d998d8 (patch) | |
| tree | 6f0ca304671576b7bea45aca286743a59505d4b9 /src/rewriter.ml | |
| parent | 587f9dc7c6409d5ef89719fd65fe7bbb8f8d86b7 (diff) | |
more shallow embedding fixes
Diffstat (limited to 'src/rewriter.ml')
| -rw-r--r-- | src/rewriter.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index 4b6598c0..dab16ae4 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -895,7 +895,8 @@ let remove_vector_concat_pat pat = E_aux (E_app_infix(length_app_exp,minus,one_exp),annot) in exp in - let subv = E_aux (E_vector_subrange (root,index_i,index_j),cannot) in + let subv = E_aux (E_app (Id_aux (Id "slice_raw",Unknown), + [root;index_i;index_j]),cannot) in let typ = (Parse_ast.Generated l,simple_annot {t = Tid "unit"}) in |