From 7dc578956e1896b8bb68102f431795fc871cad7b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 13 Mar 2020 14:53:24 +0100
Subject: Partial import inductive(..)

NB: 3 dots doesn't play well with PG's sentence detection.
---
 kernel/sorts.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/sorts.ml')

diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 466fbacca4..3a89b73bd5 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -12,6 +12,8 @@ open Univ
 
 type family = InSProp | InProp | InSet | InType
 
+let all_families = [InSProp; InProp; InSet; InType]
+
 type t =
   | SProp
   | Prop
-- 
cgit v1.2.3