From b71e68fb78ccde52f1aaa63ef26f0135b92e9be5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 8 Sep 2017 14:58:28 +0200
Subject: Parse directly to Sorts.family when appropriate.

When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
---
 intf/vernacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 2adf522b74..a02f1a9d4e 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -169,7 +169,7 @@ type option_ref_value =
 (** Identifier and optional list of bound universes. *)						 
 type plident = lident * lident list option
 
-type sort_expr = glob_sort
+type sort_expr = Sorts.family
 
 type definition_expr =
   | ProveBody of local_binder_expr list * constr_expr
-- 
cgit v1.2.3