diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-14 13:20:31 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-14 13:20:31 -0400 |
| commit | 29583c631fec665d0c08f5a679fb974c5133aed6 (patch) | |
| tree | 8e7598d558c1f9f213a71039d0f8b78539e6648a /src/Reflection/Named/WfInterp.v | |
| parent | 8c8a223fc8b4ddae385f79c700b2983bbf794862 (diff) | |
Move ContextOk to ContextDefinitions
Diffstat (limited to 'src/Reflection/Named/WfInterp.v')
| -rw-r--r-- | src/Reflection/Named/WfInterp.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Reflection/Named/WfInterp.v b/src/Reflection/Named/WfInterp.v index b8cfb7fbe..17fc43ca5 100644 --- a/src/Reflection/Named/WfInterp.v +++ b/src/Reflection/Named/WfInterp.v @@ -10,8 +10,7 @@ Section language. Context {base_type_code Name interp_base_type} {op : flat_type base_type_code -> flat_type base_type_code -> Type} {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst} - {Context : @Context base_type_code Name interp_base_type} - {ContextOk : ContextOk Context}. + {Context : @Context base_type_code Name interp_base_type}. Lemma wff_interpf_not_None {ctx : Context} {t} {e : @exprf base_type_code op Name t} (Hwf : prop_of_option (wff ctx e)) |