diff options
| author |  Jason Gross <jgross@mit.edu> | 2013-12-12 12:19:16 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2014-08-26 11:39:00 -0400 |
| commit | d2958e26d0778ae624495a34fe47ba036439a44d (patch) | |
| tree | aae509a26d8be468b6a2a94ae076c5f52ad8e2b1 /theories/Logic/Eqdep_dec.v | |
| parent | 9ef5dbb1f340971036aa0c7d4d7a0986188fd971 (diff) | |
Generalize EqdepFacts
The generalized versions are names *_one_var. We preserve backwards
compatibility by defining the old versions in terms of the generalized
ones.
This closes the rest of Bug 3019, and closes pull request #6.
Diffstat (limited to 'theories/Logic/Eqdep_dec.v')
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index e4adc8cf1..154508bb5 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -340,8 +340,8 @@ Proof. intros A eq_dec. apply eq_dep_eq__inj_pair2. apply eq_rect_eq__eq_dep_eq. - unfold Eq_rect_eq. - apply eq_rect_eq_dec. + unfold Eq_rect_eq, Eq_rect_eq_one_var. + intros; apply eq_rect_eq_dec. apply eq_dec. Qed. |