diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-29 23:18:40 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-29 23:18:40 -0400 |
| commit | b6f6fc6c463bf531698978849545ba5d06173b38 (patch) | |
| tree | 6bc1a5c847ec8c0e2f4271e9e272a11da81af156 /src/Reflection/Reify.v | |
| parent | 4ae2f20dc35546bdc4e54a3570504778286cdd37 (diff) | |
Handle Let_In in reification
Diffstat (limited to 'src/Reflection/Reify.v')
| -rw-r--r-- | src/Reflection/Reify.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index b10ab66f4..2631a8a21 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -6,6 +6,7 @@ Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.InputSyntax. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T. @@ -122,6 +123,10 @@ Ltac reifyf base_type_code interp_base_type op var e := let ex := reify_rec ex in let eC := reify_rec eC in mkLetIn ex eC + | dlet x := ?ex in @?eC x => + let ex := reify_rec ex in + let eC := reify_rec eC in + mkLetIn ex eC | pair ?a ?b => let a := reify_rec a in let b := reify_rec b in |