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

---
 kernel/cbytegen.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/cbytegen.ml')

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 7a27a3d20..881bfae19 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -498,7 +498,7 @@ let rec compile_lam env cenv lam sz cont =
     else comp_app compile_structured_constant compile_universe cenv
         (Const_ind ind) (Univ.Instance.to_array u) sz cont
 
-  | Lsort (Sorts.Prop _ as s) ->
+  | Lsort (Sorts.Prop | Sorts.Set as s) ->
     compile_structured_constant cenv (Const_sort s) sz cont
   | Lsort (Sorts.Type u) ->
     (* We represent universes as a global constant with local universes
-- 
cgit v1.2.3