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.
---
 printing/ppvernac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4c50c2f368..fa2b166dae 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -275,7 +275,7 @@ open Decl_kinds
         ) ++
           hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for")
                  ++ spc() ++ pr_smart_global ind) ++ spc() ++
-          hov 0 (keyword "Sort" ++ spc() ++ pr_glob_sort s)
+          hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s)
       | CaseScheme (dep,ind,s) ->
         (match idop with
           | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
@@ -283,7 +283,7 @@ open Decl_kinds
         ) ++
           hov 0 ((if dep then keyword "Elimination for" else keyword "Case for")
                  ++ spc() ++ pr_smart_global ind) ++ spc() ++
-          hov 0 (keyword "Sort" ++ spc() ++ pr_glob_sort s)
+          hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s)
       | EqualityScheme ind ->
         (match idop with
           | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
-- 
cgit v1.2.3