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 ++
 kernel/sorts.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'kernel')

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
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 49549e224d..fe939b1d95 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -12,6 +12,8 @@
 
 type family = InSProp | InProp | InSet | InType
 
+val all_families : family list
+
 type t = private
   | SProp
   | Prop
-- 
cgit v1.2.3