diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-11 13:38:47 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-11 13:38:47 -0400 |
| commit | 7146036f5a4555840a75b1fb564ee3c1b54623dc (patch) | |
| tree | ded017dae3c8f0fb62f173d6f9baab338773a5e4 /src/Compilers/EtaWf.v | |
| parent | df5218b25d73bc95becc6d1c9db124951dccd925 (diff) | |
s/appcontext/context/
They mean the same thing since 8.5, and appcontext is deprecated.
Diffstat (limited to 'src/Compilers/EtaWf.v')
| -rw-r--r-- | src/Compilers/EtaWf.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/EtaWf.v b/src/Compilers/EtaWf.v index e8dd2f846..1134b5d05 100644 --- a/src/Compilers/EtaWf.v +++ b/src/Compilers/EtaWf.v @@ -28,7 +28,7 @@ Section language. | _ => progress split_iff | _ => rewrite eq_interp_flat_type_eta_gen by assumption | [ H : _ |- _ ] => rewrite eq_interp_flat_type_eta_gen in H by assumption - | [ H : appcontext[interp_flat_type_eta_gen] |- _ ] + | [ H : context[interp_flat_type_eta_gen] |- _ ] => setoid_rewrite eq_interp_flat_type_eta_gen in H; [ | assumption.. ] | _ => progress break_match | [ H : wff _ _ _ |- _ ] => solve [ inversion H ] |