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

20 files changed, 55 insertions, 62 deletions

diff --git a/API/API.mli b/API/API.mli
index 8b0bef48c..e3643076a 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2763,6 +2763,7 @@ sig
   val pr_evar_info : Evd.evar_info -> Pp.t
 
   val print_constr : EConstr.constr -> Pp.t
+  val pr_sort_family : Sorts.family -> Pp.t
 
   (** [dependent m t] tests whether [m] is a subterm of [t] *)
   val dependent : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
@@ -4046,7 +4047,6 @@ sig
   val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
                    Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Constr.t Evd.in_evar_universe_context
   val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit
-  val interp_elimination_sort : Misctypes.glob_sort -> Sorts.family
   val register_constr_interp0 :
     ('r, 'g, 't) Genarg.genarg_type ->
     (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit
@@ -4142,6 +4142,7 @@ sig
   val wit_global : (Libnames.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type
   val wit_ident : Names.Id.t Genarg.uniform_genarg_type
   val wit_integer : int Genarg.uniform_genarg_type
+  val wit_sort_family : (Sorts.family, unit, unit) Genarg.genarg_type
   val wit_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type
   val wit_open_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type
   val wit_intro_pattern : (Constrexpr.constr_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.glob_constr_and_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.intro_pattern) Genarg.genarg_type
@@ -4773,6 +4774,7 @@ sig
     val global : reference Gram.entry
     val universe_level : glob_level Gram.entry
     val sort : glob_sort Gram.entry
+    val sort_family : Sorts.family Gram.entry
     val pattern : cases_pattern_expr Gram.entry
     val constr_pattern : constr_expr Gram.entry
     val lconstr_pattern : constr_expr Gram.entry
@@ -5333,7 +5335,7 @@ sig
   val lemInv_clause :
     Misctypes.quantified_hypothesis -> EConstr.constr -> Names.Id.t list -> unit Proofview.tactic
   val add_inversion_lemma_exn :
-    Names.Id.t -> Constrexpr.constr_expr -> Misctypes.glob_sort -> bool -> (Names.Id.t -> unit Proofview.tactic) ->
+    Names.Id.t -> Constrexpr.constr_expr -> Sorts.family -> bool -> (Names.Id.t -> unit Proofview.tactic) ->
     unit
 end
 
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 274ea6213..45dec5112 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -50,6 +50,8 @@ let wit_ref = make0 "ref"
 
 let wit_quant_hyp = make0 "quant_hyp"
 
+let wit_sort_family = make0 "sort_family"
+
 let wit_constr =
   make0 "constr"
 
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 1d4a29b9c..dffbd6659 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -47,6 +47,8 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
 
 val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
 
+val wit_sort_family : (Sorts.family, unit, unit) genarg_type
+
 val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
 
 val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 2adf522b7..a02f1a9d4 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
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index f637e9746..7d0728458 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -123,8 +123,8 @@ let name_colon =
 let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None
 
 GEXTEND Gram
-  GLOBAL: binder_constr lconstr constr operconstr universe_level sort global
-  constr_pattern lconstr_pattern Constr.ident
+  GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family
+  global constr_pattern lconstr_pattern Constr.ident
   closed_binder open_binders binder binders binders_fixannot
   record_declaration typeclass_constraint pattern appl_arg;
   Constr.ident:
@@ -149,6 +149,12 @@ GEXTEND Gram
       | "Type"; "@{"; u = universe; "}" -> GType u
       ] ]
   ;
+  sort_family:
+    [ [ "Set"  -> Sorts.InSet
+      | "Prop" -> Sorts.InProp
+      | "Type" -> Sorts.InType
+      ] ]
+  ;
   universe:
     [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids
       | id = name -> [id]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b9a162bec..5b044d2f0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -340,13 +340,13 @@ GEXTEND Gram
   ;
   scheme_kind:
     [ [ IDENT "Induction"; "for"; ind = smart_global;
-          IDENT "Sort"; s = sort-> InductionScheme(true,ind,s)
+          IDENT "Sort"; s = sort_family-> InductionScheme(true,ind,s)
       | IDENT "Minimality"; "for"; ind = smart_global;
-          IDENT "Sort"; s = sort-> InductionScheme(false,ind,s)
+          IDENT "Sort"; s = sort_family-> InductionScheme(false,ind,s)
       | IDENT "Elimination"; "for"; ind = smart_global;
-          IDENT "Sort"; s = sort-> CaseScheme(true,ind,s)
+          IDENT "Sort"; s = sort_family-> CaseScheme(true,ind,s)
       | IDENT "Case"; "for"; ind = smart_global;
-          IDENT "Sort"; s = sort-> CaseScheme(false,ind,s)
+          IDENT "Sort"; s = sort_family-> CaseScheme(false,ind,s)
       | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ]
   ;
   (* Various Binders *)
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 81f02bf95..0d24599ea 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -471,6 +471,7 @@ module Constr =
     let global = make_gen_entry uconstr "global"
     let universe_level = make_gen_entry uconstr "universe_level"
     let sort = make_gen_entry uconstr "sort"
+    let sort_family = make_gen_entry uconstr "sort_family"
     let pattern = Gram.entry_create "constr:pattern"
     let constr_pattern = gec_constr "constr_pattern"
     let lconstr_pattern = gec_constr "lconstr_pattern"
@@ -631,6 +632,7 @@ let () =
   Grammar.register0 wit_ident (Prim.ident);
   Grammar.register0 wit_var (Prim.var);
   Grammar.register0 wit_ref (Prim.reference);
+  Grammar.register0 wit_sort_family (Constr.sort_family);
   Grammar.register0 wit_constr (Constr.constr);
   Grammar.register0 wit_red_expr (Vernac_.red_expr);
   ()
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 445818e13..897e42c30 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -225,6 +225,7 @@ module Constr :
     val global : reference Gram.entry
     val universe_level : glob_level Gram.entry
     val sort : glob_sort Gram.entry
+    val sort_family : Sorts.family Gram.entry
     val pattern : cases_pattern_expr Gram.entry
     val constr_pattern : constr_expr Gram.entry
     val lconstr_pattern : constr_expr Gram.entry
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
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 79d2c3333..7cd35f530 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -222,18 +222,6 @@ let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
   | None -> new_univ_level_variable ?loc univ_rigid evd
   | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s)
 
-let interp_sort ?loc evd = function
-  | GProp -> evd, Prop Null
-  | GSet -> evd, Prop Pos
-  | GType n -> 
-    let evd, u = interp_universe ?loc evd n in
-      evd, Type u
-
-let interp_elimination_sort = function
-  | GProp -> InProp
-  | GSet  -> InSet
-  | GType _ -> InType
-
 type inference_hook = env -> evar_map -> evar -> evar_map * constr
 
 type inference_flags = {
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7395e94a0..5822f5add 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -18,7 +18,6 @@ open Evd
 open EConstr
 open Glob_term
 open Evarutil
-open Misctypes
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
@@ -119,9 +118,6 @@ val ise_pretype_gen :
 
 (** To embed constr in glob_constr *)
 
-val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts
-val interp_elimination_sort : glob_sort -> sorts_family
-
 val register_constr_interp0 :
   ('r, 'g, 't) Genarg.genarg_type ->
     (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4c50c2f36..fa2b166da 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()
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index aeb80ae57..967ec2a71 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -248,9 +248,9 @@ let add_inversion_lemma_exn na com comsort bool tac =
   let env = Global.env () in
   let evd = ref (Evd.from_env env) in
   let c = Constrintern.interp_type_evars env evd com in
-  let sigma, sort = Pretyping.interp_sort !evd comsort in
+  let evd, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env !evd comsort in
   try
-    add_inversion_lemma na env sigma c sort bool tac
+    add_inversion_lemma na env evd c sort bool tac
   with
     |   UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
 	  user_err ~hdr:"Inv needs Nodep Prop Set" s
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 41b0e09b4..8745ad397 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -15,5 +15,5 @@ val lemInv_clause :
   quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
 
 val add_inversion_lemma_exn :
-  Id.t -> constr_expr -> glob_sort -> bool -> (Id.t -> unit Proofview.tactic) ->
+  Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
     unit
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 *)