Merge PR #1037: Parse directly to Sorts.family when appropriate.

5 files changed, 20 insertions, 23 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 513fce248..ef1654fdf 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -11,7 +11,6 @@ open Tactics
 open Context.Rel.Declaration
 open Indfun_common
 open Functional_principles_proofs
-open Misctypes
 
 module RelDecl = Context.Rel.Declaration
 
@@ -463,7 +462,7 @@ let get_funs_constant mp dp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list =
+let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_constants definition_entry list =
   let env = Global.env () in
   let funs = List.map fst fas in
   let first_fun = List.hd funs in
@@ -500,7 +499,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
   let i = ref (-1) in
   let sorts =
     List.rev_map (fun (_,x) ->
-		  Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd (Pretyping.interp_elimination_sort x)
+		  Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x
 	     )
       fas
   in
@@ -674,7 +673,7 @@ let build_case_scheme fa =
   let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
   let sorts =
     (fun (_,_,x) ->
-       Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
+       Universes.new_sort_in_family x
     )
       fa
   in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 5a7ffe059..2eb1b7935 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Misctypes
 
 val generate_functional_principle :
   Evd.evar_map ref -> 
@@ -37,8 +36,7 @@ val compute_new_princ_type_from_rel : constr array -> Sorts.t array ->
 exception No_graph_found
 
 val make_scheme :   Evd.evar_map ref ->
- (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list
-
-val build_scheme : (Id.t*Libnames.reference*glob_sort) list ->  unit
-val build_case_scheme : (Id.t*Libnames.reference*glob_sort)  ->  unit
+ (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list
 
+val build_scheme : (Id.t*Libnames.reference*Sorts.family) list ->  unit
+val build_case_scheme : (Id.t*Libnames.reference*Sorts.family)  ->  unit
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 16d9f200f..62ecaa552 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
 
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8dea6c90f..5f8d50da1 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -797,7 +797,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	       (fun entry ->
 		  (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type ))
 	       )
-	       (make_scheme evd (Array.map_to_list (fun const -> const,GType []) funs))
+	       (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
 	    )
 	)
     in
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 99e444010..b4c6f9c90 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -403,38 +403,38 @@ open Leminv
 
 let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
 
-VERNAC ARGUMENT EXTEND sort
-| [ "Set" ] -> [ GSet ]
-| [ "Prop" ] -> [ GProp ]
-| [ "Type" ] -> [ GType [] ]
-END
+(*VERNAC ARGUMENT EXTEND sort_family
+| [ "Set" ] -> [ InSet ]
+| [ "Prop" ] -> [ InProp ]
+| [ "Type" ] -> [ InType ]
+END*)
 
 VERNAC COMMAND EXTEND DeriveInversionClear
-| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
+| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => [ seff na ]
   -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ]
-  -> [ add_inversion_lemma_exn na c GProp false inv_clear_tac ]
+  -> [ add_inversion_lemma_exn na c InProp false inv_clear_tac ]
 END
 
 VERNAC COMMAND EXTEND DeriveInversion
-| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
+| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => [ seff na ]
   -> [ add_inversion_lemma_exn na c s false inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
-  -> [ add_inversion_lemma_exn na c GProp false inv_tac ]
+  -> [ add_inversion_lemma_exn na c InProp false inv_tac ]
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversion
-| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
+| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => [ seff na ]
   -> [ add_inversion_lemma_exn na c s true dinv_tac ]
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversionClear
-| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
+| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => [ seff na ]
   -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
 END