diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-30 12:35:06 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-30 12:35:06 -0400 |
| commit | 7a9faafa8a3507bc20ae15bbe71200d9c4b5a12b (patch) | |
| tree | cb1efeaf96cea972407717c9fa967cc1d4c8baf3 /src/Reflection/Z/Reify.v | |
| parent | 71b2c82fab79b17a8eef0c596f6bb81291ca9968 (diff) | |
Generalize InputSyntax.Compile_correct
Diffstat (limited to 'src/Reflection/Z/Reify.v')
| -rw-r--r-- | src/Reflection/Z/Reify.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v index 9500b2b88..87c3e29e7 100644 --- a/src/Reflection/Z/Reify.v +++ b/src/Reflection/Z/Reify.v @@ -27,4 +27,4 @@ Ltac Reify e := let v := Reflection.Reify.Reify base_type interp_base_type op e in constr:((*Inline _*) ((*CSE _*) (InlineConst (Linearize v)))). Ltac Reify_rhs := - etransitivity; [ | Reflection.Reify.Reify_rhs base_type interp_base_type op interp_op ]. + Reflection.Reify.Reify_rhs_gen Reify ltac:(fun _ => idtac) interp_op ltac:(fun tac => try tac ()). |