diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-05 18:27:10 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 18:27:10 -0700 |
| commit | 0cb8d2bd781c8094e32ff1de78e461bd44d3ea7e (patch) | |
| tree | c1dac430375ffbec14defee5e38eacb3b32a4274 /src | |
| parent | 4ba2afbd76ffaca05db5a6f9ddbe52b503dfaeb5 (diff) | |
Reorder WfProofs arguments
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/WfProofs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Reflection/WfProofs.v b/src/Reflection/WfProofs.v index dc5eed88c..83c253c43 100644 --- a/src/Reflection/WfProofs.v +++ b/src/Reflection/WfProofs.v @@ -22,11 +22,11 @@ Section language. Context {var1 var2 : base_type_code -> Type}. Local Hint Constructors Syntax.wff. Lemma wff_in_impl_Proper G0 G1 {t} e1 e2 - (H : forall x, List.In x G0 -> List.In x G1) : @wff var1 var2 G0 t e1 e2 + -> (forall x, List.In x G0 -> List.In x G1) -> @wff var1 var2 G1 t e1 e2. Proof. - intro wf; revert G1 H; induction wf; + intro wf; revert G1; induction wf; repeat match goal with | _ => setoid_rewrite List.in_app_iff | _ => progress intros |