Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles des sortes (InProp, InSet, InType)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 18 insertions, 18 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 9b6466f47f..d2e451dd9e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -554,12 +554,12 @@ let instantiate_inductive_section_params t ind =
 (* Eliminations. *)
 
 let eliminations =
-  [ (ElimOnProp,"_ind") ; (ElimOnSet,"_rec") ; (ElimOnType,"_rect") ]
+  [ (InProp,"_ind") ; (InSet,"_rec") ; (InType,"_rect") ]
 
 let elimination_suffix = function
-  | ElimOnProp -> "_ind"
-  | ElimOnSet  -> "_rec"
-  | ElimOnType -> "_rect"
+  | InProp -> "_ind"
+  | InSet  -> "_rec"
+  | InType -> "_rect"
 
 let make_elimination_ident id s = add_suffix id (elimination_suffix s)
   
@@ -583,7 +583,7 @@ let declare_one_elimination mispec =
   List.iter
     (fun (sort,suff) -> 
        if List.mem sort kelim then
-	 declare (mindstr^suff) (make_elim (sort_of_elimination sort)))
+	 declare (mindstr^suff) (make_elim (new_sort_in_family sort)))
     eliminations
 
 let declare_eliminations sp =
diff --git a/library/declare.mli b/library/declare.mli
index b347456ce5..4d7043eae7 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -119,7 +119,7 @@ val path_of_inductive_path : inductive_path -> mutual_inductive_path
 val path_of_constructor_path : constructor_path -> mutual_inductive_path
 
 (* Look up function for the default elimination constant *)
-val elimination_suffix : elimination_sorts -> string
+val elimination_suffix : sorts_family -> string
 val make_elimination_ident :
-  inductive_ident:identifier -> elimination_sorts -> identifier
-val lookup_eliminator : Environ.env -> inductive -> elimination_sorts -> constr
+  inductive_ident:identifier -> sorts_family -> identifier
+val lookup_eliminator : Environ.env -> inductive -> sorts_family -> constr
diff --git a/library/indrec.ml b/library/indrec.ml
index f15ed4b53f..96a188da79 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -44,7 +44,7 @@ let mis_make_case_com depopt env sigma mispec kind =
     raise
       (InductiveError
 	 (NotAllowedCaseAnalysis
-	    (dep,(sort_of_elimination kind),mis_inductive mispec)));
+	    (dep,(new_sort_in_family kind),mis_inductive mispec)));
 
   let nbargsprod = mis_nrealargs mispec + 1 in
 
@@ -75,7 +75,7 @@ let mis_make_case_com depopt env sigma mispec kind =
       mkLambda_string "f" t
 	(add_branch (push_rel (Anonymous, None, t) env) (k+1))
   in
-  let typP = make_arity env' dep indf (sort_of_elimination kind) in
+  let typP = make_arity env' dep indf (new_sort_in_family kind) in
   it_mkLambda_or_LetIn_name env 
     (mkLambda_string "P" typP
        (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
@@ -372,7 +372,7 @@ let mis_make_indrec env sigma listdepkind mispec =
     let rec put_arity env i = function 
       | (mispeci,dep,kinds)::rest -> 
 	  let indf = make_ind_family (mispeci,extended_rel_list i lnamespar) in
-	  let typP = make_arity env dep indf (sort_of_elimination kinds) in
+	  let typP = make_arity env dep indf (new_sort_in_family kinds) in
 	  mkLambda_string "P" typP
 	    (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
       | [] -> 
@@ -438,7 +438,7 @@ let check_arities listdepkind =
        let kelim = mis_kelim mispeci in
        if not (List.exists ((=) kind) kelim) then
 	 raise
-	   (InductiveError (BadInduction (dep, id, sort_of_elimination kind))))
+	   (InductiveError (BadInduction (dep, id, new_sort_in_family kind))))
     listdepkind
 
 let build_mutual_indrec env sigma = function 
@@ -461,8 +461,8 @@ let build_mutual_indrec env sigma = function
   | _ -> anomaly "build_indrec expects a non empty list of inductive types"
 
 let build_indrec env sigma mispec =
-  let kind = elimination_of_sort (mis_sort mispec) in
-  let dep = kind <> ElimOnProp in
+  let kind = family_of_sort (mis_sort mispec) in
+  let dep = kind <> InProp in
   List.hd (mis_make_indrec env sigma [(mispec,dep,kind)] mispec)
 
 (**********************************************************************)
diff --git a/library/indrec.mli b/library/indrec.mli
index e53b7d2a8c..aa3a0b6f1f 100644
--- a/library/indrec.mli
+++ b/library/indrec.mli
@@ -21,9 +21,9 @@ open Evd
 
 (* These functions build elimination predicate for Case tactic *)
 
-val make_case_dep : env -> 'a evar_map -> inductive -> elimination_sorts -> constr
-val make_case_nodep : env -> 'a evar_map -> inductive -> elimination_sorts -> constr
-val make_case_gen : env -> 'a evar_map -> inductive -> elimination_sorts -> constr
+val make_case_dep : env -> 'a evar_map -> inductive -> sorts_family -> constr
+val make_case_nodep : env -> 'a evar_map -> inductive -> sorts_family -> constr
+val make_case_gen : env -> 'a evar_map -> inductive -> sorts_family -> constr
 
 (* This builds an elimination scheme associated (using the own arity
    of the inductive) *)
@@ -34,7 +34,7 @@ val instanciate_indrec_scheme : sorts -> int -> constr -> constr
 (* This builds complex [Scheme] *)
 
 val build_mutual_indrec : 
-  env -> 'a evar_map -> (inductive * bool * elimination_sorts) list
+  env -> 'a evar_map -> (inductive * bool * sorts_family) list
     -> constr list
 
 (* These are for old Case/Match typing *)