From af0a04b8e16c2554e0c747da6d625799b332f5fe Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 11 Oct 2017 19:41:23 +0200
Subject: Remove Sorts.contents

---
 pretyping/coercion.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/coercion.ml')

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index bf9e37aa7..5c4cbefad 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -209,8 +209,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
       match (EConstr.kind !evdref x, EConstr.kind !evdref y) with
       | Sort s, Sort s' ->
         (match ESorts.kind !evdref s, ESorts.kind !evdref s' with
-	| Prop x, Prop y when x == y -> None
-	| Prop _, Type _ -> None
+        | Prop, Prop | Set, Set -> None
+        | (Prop | Set), Type _ -> None
 	| Type x, Type y when Univ.Universe.equal x y -> None (* false *)
 	| _ -> subco ())
       | Prod (name, a, b), Prod (name', a', b') ->
-- 
cgit v1.2.3