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.
---
 plugins/funind/g_indfun.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/g_indfun.ml4')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 16d9f200f3..62ecaa552b 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -166,11 +166,11 @@ END
 let pr_fun_scheme_arg (princ_name,fun_name,s) =
   Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
   Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++
-  Ppconstr.pr_glob_sort s
+  Termops.pr_sort_family s
 
 VERNAC ARGUMENT EXTEND fun_scheme_arg
 PRINTED BY pr_fun_scheme_arg
-| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ]
+| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> [ (princ_name,fun_name,s) ]
 END
 
 
-- 
cgit v1.2.3