diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-28 22:40:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-28 22:40:02 -0400 |
| commit | b54e6b8b55c957901cfc8a1504f9cd1b281c5cdd (patch) | |
| tree | 6915248e4f23e602a7c86f9f978dfb504aaf20d1 /src/Reflection/InputSyntax.v | |
| parent | 0fb8dfb5e3dd975801d56d5fca0dc2990422350a (diff) | |
Add interp_type_gen_rel_pointwise2, *_gen => *
Diffstat (limited to 'src/Reflection/InputSyntax.v')
| -rw-r--r-- | src/Reflection/InputSyntax.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index ad101e62f..15f7515b3 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -22,7 +22,8 @@ Section language. Context (interp_base_type : base_type_code -> Type). Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Type). Local Notation interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type := (interp_flat_type_gen interp_base_type). + Local Notation interp_flat_type_gen := interp_flat_type. + Local Notation interp_flat_type := (interp_flat_type interp_base_type). Section expr. Context {var : flat_type -> Type}. @@ -108,7 +109,7 @@ Section language. : Syntax.Interp interp_op (Compile e) = Interp interp_op e. Proof. unfold Interp, Compile, Syntax.Interp; simpl. - pose (e (interp_flat_type_gen interp_base_type)) as E. + pose (e interp_flat_type) as E. repeat match goal with |- context[e ?f] => change (e f) with E end. refine match E with | Abs _ _ _ => fun x : Prop => x (* small inversions *) |