diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-06 11:59:08 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-06 11:59:08 -0700 |
| commit | a1c7bd0d0cade0df94f36d0dd34ce775817fb391 (patch) | |
| tree | 3c380c2512cb045385ecfb6e633619f38b35226e /src | |
| parent | e79aa03ae5575cf37065894c198a8b3ca8372cea (diff) | |
Fix for 8.6 (context (correctly) no longer defaults to type_scope)
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/LinearizeWf.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v index f7860db30..2a3d193ac 100644 --- a/src/Reflection/LinearizeWf.v +++ b/src/Reflection/LinearizeWf.v @@ -254,7 +254,7 @@ Section language. small_inversion_helper wf G' e2; t_fin idtac; repeat match goal with - | [ H : context[_ -> wff _ (inline_constf ?e) (inline_constf _)], e2 : exprf _ |- _ ] + | [ H : context[(_ -> wff _ (inline_constf ?e) (inline_constf _))%type], e2 : exprf _ |- _ ] => is_var e; not constr_eq e e2; specialize (H e2) | [ H : context[wff _ (@inline_constf ?A ?B ?C ?D ?E ?e) _] |- context[match @inline_constf ?A ?B ?C ?D ?E ?e with _ => _ end] ] => destruct (@inline_constf A B C D E e) |