diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-10 14:34:21 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-10 15:10:30 -0500 |
| commit | ccee9c2e2fd49ae7a918287a42f9f138a4f5bc1a (patch) | |
| tree | 91e406fcde58a3cb3b7cc612872395e73811421d /src | |
| parent | 78cd7077c6fbaba2d1af540ba622db2ea03a3fbb (diff) | |
Handle more base types in Z.Reify
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Z/Reify.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Compilers/Z/Reify.v b/src/Compilers/Z/Reify.v index 7180ac115..8fb02536d 100644 --- a/src/Compilers/Z/Reify.v +++ b/src/Compilers/Z/Reify.v @@ -58,6 +58,11 @@ Ltac base_reify_op op op_head extra ::= Ltac base_reify_type T ::= lazymatch T with | Z => TZ + | Z.Syntax.interp_base_type TZ => TZ + | ?T + => lazymatch (eval hnf in T) with + | Z => TZ + end end. Ltac Reify' e := let e := (eval cbv beta delta [Z.add_get_carry Z.sub_get_borrow] in e) in |