diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 58b6d076c5..afd0ecf046 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -376,7 +376,7 @@ Proof. (eq_sym (UIP (eq_refl x) (eq_refl x)))). - destruct z. unfold e. destruct (UIP _ _). reflexivity. - change - (match eq_refl x as y' in _ = x' return y' = y' -> Type with + (match eq_refl x as y' in _ = x' return y' = y' -> Prop with | eq_refl => fun z => z = (eq_refl (eq_refl x)) end (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) (eq_sym (UIP (eq_refl x) (eq_refl x))))). |