diff options
Diffstat (limited to 'src/Compilers/Named/WfInterp.v')
| -rw-r--r-- | src/Compilers/Named/WfInterp.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Compilers/Named/WfInterp.v b/src/Compilers/Named/WfInterp.v index 580dcb438..e9cd8737c 100644 --- a/src/Compilers/Named/WfInterp.v +++ b/src/Compilers/Named/WfInterp.v @@ -15,7 +15,7 @@ Section language. Lemma wff_interpf_not_None {ctx : Context} {t} {e : @exprf base_type_code op Name t} (Hwf : prop_of_option (wff ctx e)) - : @interpf base_type_code interp_base_type op Name Context interp_op ctx t e <> None. + : @interpf base_type_code interp_base_type op Name Context interp_op t ctx e <> None. Proof using Type. revert dependent ctx; induction e; repeat first [ progress intros @@ -34,7 +34,7 @@ Section language. Lemma wf_interp_not_None {ctx : Context} {t} {e : @expr base_type_code op Name t} (Hwf : wf ctx e) v - : @interp base_type_code interp_base_type op Name Context interp_op ctx t e v <> None. + : @interp base_type_code interp_base_type op Name Context interp_op t ctx e v <> None. Proof using Type. destruct e; unfold interp, wf in *; apply wff_interpf_not_None; auto. Qed. |