From 2b80095f5dbfb996643309bfae6f45f62e2ecdb1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 18 Nov 2020 13:48:54 +0100
Subject: Reserve "sort_expr" for uninterned universes

---
 vernac/vernacexpr.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index defb0691c0..89c09bb169 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -129,8 +129,6 @@ type option_setting =
 
 (** Identifier and optional list of bound universes and constraints. *)
 
-type sort_expr = Sorts.family
-
 type definition_expr =
   | ProveBody of local_binder_expr list * constr_expr
   | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
@@ -210,8 +208,8 @@ type proof_end =
   | Proved of opacity_flag * lident option
 
 type scheme =
-  | InductionScheme of bool * qualid or_by_notation * sort_expr
-  | CaseScheme of bool * qualid or_by_notation * sort_expr
+  | InductionScheme of bool * qualid or_by_notation * Sorts.family
+  | CaseScheme of bool * qualid or_by_notation * Sorts.family
   | EqualityScheme of qualid or_by_notation
 
 type section_subset_expr =
-- 
cgit v1.2.3