diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-24 11:11:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-24 21:05:06 +0200 |
| commit | 31e4222d35b614efa94a1d68b5d6491ea9e46bfa (patch) | |
| tree | f5b60f2a6ab94ad7f8ef6a0c9094804f204140be /theories/Logic | |
| parent | c955779074833066e9db81c9fb1b32493cfebfa2 (diff) | |
Return a Prop not an arbitrary Type, and correct a typo.
Diffstat (limited to 'theories/Logic')
| -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 58b6d076c..afd0ecf04 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))))). |