diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-26 18:19:54 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-26 18:20:08 -0500 |
| commit | 39c70ae2abd720ec76e01c85d2aa0e56aeae3414 (patch) | |
| tree | b8ca8c8c4e935a078813d1f753f29db7e95f91d4 /src/Reflection/WfInversion.v | |
| parent | 0cf72bdda642db646e25cba8af97f3c63d88764d (diff) | |
Split off some bits of Reflection.Syntax
Also split off some bits of Util.Tactics
Diffstat (limited to 'src/Reflection/WfInversion.v')
| -rw-r--r-- | src/Reflection/WfInversion.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Reflection/WfInversion.v b/src/Reflection/WfInversion.v index 4a253f28b..bf396d52e 100644 --- a/src/Reflection/WfInversion.v +++ b/src/Reflection/WfInversion.v @@ -1,4 +1,5 @@ Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Wf. Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Option. @@ -52,7 +53,7 @@ Section language. => { pf : tx1 = tx2 | wff G (eq_rect _ exprf ex1 _ pf) ex2 /\ (forall x1 x2, - wff (flatten_binding_list base_type_code x1 x2 ++ G)%list + wff (flatten_binding_list x1 x2 ++ G)%list (eC1 x1) (eC2 (eq_rect _ _ x2 _ pf))) } | None => False end |