From b71e68fb78ccde52f1aaa63ef26f0135b92e9be5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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.
---
 vernac/indschemes.ml  | 12 +++++-------
 vernac/indschemes.mli |  3 +--
 2 files changed, 6 insertions(+), 9 deletions(-)

(limited to 'vernac')

diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 6ea8bc7f2..facebd096 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -30,7 +30,6 @@ open Globnames
 open Goptions
 open Nameops
 open Termops
-open Pretyping
 open Nametab
 open Smartlocate
 open Vernacexpr
@@ -345,24 +344,23 @@ requested
       let names inds recs isdep y z =
         let ind = smart_global_inductive y in
         let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in
-        let z' = interp_elimination_sort z in
         let suffix = (
           match sort_of_ind with
           | InProp ->
-              if isdep then (match z' with
+              if isdep then (match z with
               | InProp -> inds ^ "_dep"
               | InSet  -> recs ^ "_dep"
               | InType -> recs ^ "t_dep")
-              else ( match z' with
+              else ( match z with
               | InProp -> inds
               | InSet -> recs
               | InType -> recs ^ "t" )
           | _ ->
-              if isdep then (match z' with
+              if isdep then (match z with
               | InProp -> inds
               | InSet -> recs
               | InType -> recs ^ "t" )
-              else (match z' with
+              else (match z with
               | InProp -> inds ^ "_nodep"
               | InSet -> recs ^ "_nodep"
               | InType -> recs ^ "t_nodep")
@@ -392,7 +390,7 @@ let do_mutual_induction_scheme lnamedepindsort =
 	      evd, (ind,u), Some u
 	 | Some ui -> evd, (ind, ui), inst
        in
-          (evd, (indu,dep,interp_elimination_sort sort) :: l, inst))
+          (evd, (indu,dep,sort) :: l, inst))
     lnamedepindsort (Evd.from_env env0,[],None)
   in
   let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index 076e4938f..91c4c5825 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -11,7 +11,6 @@ open Names
 open Term
 open Environ
 open Vernacexpr
-open Misctypes
 
 (** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
 
@@ -32,7 +31,7 @@ val declare_rewriting_schemes : inductive -> unit
 (** Mutual Minimality/Induction scheme *)
 
 val do_mutual_induction_scheme :
-  (Id.t located * bool * inductive * glob_sort) list -> unit
+  (Id.t located * bool * inductive * Sorts.family) list -> unit
 
 (** Main calls to interpret the Scheme command *)
 
-- 
cgit v1.2.3