diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-01 16:58:06 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-01 16:58:06 -0500 |
| commit | e9b9ddb4fd3284e921db44a60a0ce1bc37fc8c64 (patch) | |
| tree | 838468020d899299cb745320e1343cfce53f32ac | |
| parent | 2a7e11ea7f0d1ccf2b41153b23fb18447c7a7153 (diff) | |
Adjust implicits of flatten_binding_list_same_in_eq
| -rw-r--r-- | src/Reflection/WfProofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/WfProofs.v b/src/Reflection/WfProofs.v index 84198df19..680a16f83 100644 --- a/src/Reflection/WfProofs.v +++ b/src/Reflection/WfProofs.v @@ -226,7 +226,7 @@ Section language. Qed. Lemma flatten_binding_list_same_in_eq - {var} T x t a b + {var} {T x t a b} : List.In (existT _ t (a, b)) (@flatten_binding_list base_type_code var var T x x) -> a = b. Proof. intro; eapply flatten_binding_list_In_eq_iff; eauto. Qed. End language. |