diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-31 00:13:58 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-31 00:13:58 -0400 |
| commit | 0dfe1ce918aaabd9223dc49d82b613bbc85a9c13 (patch) | |
| tree | f7fed7ee36fbca9979b29abf4c0b99b780e7e05f /src/Reflection/Syntax.v | |
| parent | d7670f26f566a94e989a10fda2c45ff6c369aae9 (diff) | |
Interpret syntax with Let_In
Diffstat (limited to 'src/Reflection/Syntax.v')
| -rw-r--r-- | src/Reflection/Syntax.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 013c91b21..35277b8d2 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -1,6 +1,7 @@ (** * PHOAS Representation of Gallina *) Require Import Coq.Strings.String Coq.Classes.RelationClasses Coq.Classes.Morphisms. Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. @@ -184,7 +185,7 @@ Section language. | Const _ x => x | Var _ x => x | Op _ _ op args => @interp_op _ _ op (@interpf _ args) - | LetIn _ ex _ eC => let x := @interpf _ ex in @interpf _ (eC x) + | LetIn _ ex _ eC => dlet x := @interpf _ ex in @interpf _ (eC x) | Pair _ ex _ ey => (@interpf _ ex, @interpf _ ey) end. Fixpoint interp {t} (e : @expr interp_type t) : interp_type t |