Utilisation d'un type spécifique (elimination_sorts) pour caractériser les éliminations, pour éviter les collisions avec les univers

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

4 files changed, 19 insertions, 14 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index c0584cd98b..c2c21d9fd5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -57,7 +57,7 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
 	else error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
         let hdcncls = string_head hdcncl in 
-	let suffix = Declare.elimination_suffix (sort_of_goal gl) in
+	let suffix = Declare.elimination_suffix (elimination_sort_of_goal gl)in
         let elim =
 	  if lft2rgt then
             pf_global gl (id_of_string (hdcncls^suffix^"_r"))
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 234c9dcd1d..6e3d331218 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -309,9 +309,13 @@ let elim_sign ity i =
   let recarg = mis_recarg (lookup_mind_specif ity (Global.env())) in
   analrec [] recarg.(i-1)
 
-let sort_of_goal gl = 
+let elimination_sort_of_goal gl = 
   match kind_of_term (hnf_type_of gl (pf_concl gl)) with 
-    | IsSort s -> s
+    | IsSort s ->
+	(match s with
+	   | Prop Null -> ElimOnProp
+	   | Prop Pos -> ElimOnSet
+	   | Type _ -> ElimOnType)
     | _        -> anomaly "goal should be a type"
 
 
@@ -374,7 +378,7 @@ let general_elim_then_using
 
 let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
   let (ind,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
-  let elim = lookup_eliminator (pf_env gl) ind (sort_of_goal gl) in
+  let elim = lookup_eliminator (pf_env gl) ind (elimination_sort_of_goal gl) in
   general_elim_then_using
     elim elim_sign tac predicate (indbindings,elimbindings) c gl
 
@@ -386,7 +390,7 @@ let case_then_using tac predicate (indbindings,elimbindings) c gl =
   (* finding the case combinator *)
   let (ity,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let sigma = project gl in 
-  let sort  = sort_of_goal gl  in
+  let sort  = elimination_sort_of_goal gl  in
   let elim  = Indrec.make_case_gen (pf_env gl) sigma ity sort in  
   general_elim_then_using 
     elim case_sign tac predicate (indbindings,elimbindings) c gl
@@ -395,7 +399,7 @@ let case_nodep_then_using tac predicate (indbindings,elimbindings) c gl =
   (* finding the case combinator *)
   let (ity,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let sigma = project gl in 
-  let sort  = sort_of_goal gl  in
+  let sort  = elimination_sort_of_goal gl  in
   let elim  = Indrec.make_case_nodep (pf_env gl) sigma ity sort in  
   general_elim_then_using 
     elim case_sign tac predicate (indbindings,elimbindings) c gl
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 9bc572c6a1..54b66539b8 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -119,7 +119,7 @@ type branch_assumptions = {
   recargs   : identifier list; (* the RECURSIVE constructor arguments *)
   indargs   : identifier list} (* the inductive arguments *)
 
-val sort_of_goal      : goal sigma -> sorts
+val elimination_sort_of_goal : goal sigma -> Declarations.elimination_sorts
 (*i val suff              : goal sigma -> constr -> string i*)
 
 val general_elim_then_using :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a7f2fb9766..09879fe390 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1058,7 +1058,7 @@ let general_elim (c,lbindc) (elimc,lbindelimc) gl =
 let default_elim (c,lbindc)  gl = 
   let env = pf_env gl in
   let (ind,t) = reduce_to_quantified_ind env (project gl) (pf_type_of gl c) in
-  let s = sort_of_goal gl in
+  let s = elimination_sort_of_goal gl in
   let elimc =
     try lookup_eliminator env ind s 
     with Not_found -> 
@@ -1069,7 +1069,8 @@ let default_elim (c,lbindc)  gl =
            pr_id id; 'sPC;
 	   'sTR "The elimination of the inductive definition :";
            pr_id base; 'sPC; 'sTR "on sort "; 
-           'sPC; print_sort s ; 'sTR " is probably not allowed" >]
+           'sPC; print_sort (Declarations.sort_of_elimination s) ;
+	   'sTR " is probably not allowed" >]
   in  general_elim (c,lbindc) (elimc,[]) gl
 
 
@@ -1422,8 +1423,8 @@ let induction_from_context isrec style hyp0 gl =
   let (mind,typ0) = pf_reduce_to_quantified_ind gl tmptyp0 in
   let indvars = find_atomic_param_of_ind mind (snd (decompose_prod typ0)) in
   let elimc =
-    if isrec then lookup_eliminator env mind (sort_of_goal gl)
-    else Indrec.make_case_gen env (project gl) mind (sort_of_goal gl)
+    if isrec then lookup_eliminator env mind (elimination_sort_of_goal gl)
+    else Indrec.make_case_gen env (project gl) mind (elimination_sort_of_goal gl)
   in
   let elimt = pf_type_of gl elimc in
   let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars env in
@@ -1533,7 +1534,7 @@ let general_case_analysis (c,lbindc) gl =
   let env = pf_env gl in
   let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   let sigma    = project gl in 
-  let sort     = sort_of_goal gl in
+  let sort     = elimination_sort_of_goal gl in
   let elim     = Indrec.make_case_gen env sigma mind sort in 
   general_elim (c,lbindc) (elim,[]) gl
     
@@ -1585,7 +1586,7 @@ let elim_scheme_type elim t gl =
 
 let elim_type t gl =
   let (ind,t) = pf_reduce_to_atomic_ind gl t in
-  let elimc = lookup_eliminator (pf_env gl) ind (sort_of_goal gl) in
+  let elimc = lookup_eliminator (pf_env gl) ind (elimination_sort_of_goal gl) in
   elim_scheme_type elimc t gl
 
 let dyn_elim_type = function
@@ -1596,7 +1597,7 @@ let dyn_elim_type = function
 let case_type t gl =
   let (ind,t) = pf_reduce_to_atomic_ind gl t in
   let env = pf_env gl in
-  let elimc = Indrec.make_case_gen env (project gl) ind (sort_of_goal gl) in 
+  let elimc = Indrec.make_case_gen env (project gl) ind (elimination_sort_of_goal gl) in 
   elim_scheme_type elimc t gl
 
 let dyn_case_type = function