- Fixing bug #2139 (kernel-based test of well-formation of elimination

  predicate called from proof refiner was failing because it was not
  aware of evars instantiation; I added a nf_evar in 8.2 branch but for
  the trunk, I propose to remove the elimination predicate
  well-formation test; we therefore assume that tactics build correct
  elimination predicates in Case, is it not too much demanding?).
- Seized the opportunity to remove dead kernel code about non dependent
  elimination predicates (all predicates are stored dependent by
  default since a few years now).
- Anecdotic complement to commit 12229 (removal of obsolete comment).



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

2 files changed, 15 insertions, 18 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 8024ae266c..23cd99d1e9 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -308,10 +308,7 @@ let is_correct_arity env c pj ind specif params =
             try conv env a1 dep_ind
             with NotConvertible -> raise (LocalArity None) in
 	  check_allowed_sort ksort specif;
-	  (true, Constraint.union u univ)
-      | Sort s', [] ->
-	  check_allowed_sort (family_of_sort s') specif;
-	  (false, u)
+	  Constraint.union u univ
       | _ ->
 	  raise (LocalArity None)
   in 
@@ -325,38 +322,34 @@ let is_correct_arity env c pj ind specif params =
 
 (* [p] is the predicate, [i] is the constructor number (starting from 0),
    and [cty] is the type of the constructor (params not instantiated) *)
-let build_branches_type ind (_,mip as specif) params dep p =
+let build_branches_type ind (_,mip as specif) params p =
   let build_one_branch i cty =
     let typi = full_constructor_instantiate (ind,specif,params) cty in
     let (args,ccl) = decompose_prod_assum typi in
     let nargs = rel_context_length args in
     let (_,allargs) = decompose_app ccl in
     let (lparams,vargs) = list_chop (inductive_params specif) allargs in
-    let cargs =
-      if dep then
-        let cstr = ith_constructor_of_inductive ind (i+1) in
-        let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in
-        vargs @ [dep_cstr]
-      else
-        vargs in
+    let cargs = 
+      let cstr = ith_constructor_of_inductive ind (i+1) in
+      let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in
+      vargs @ [dep_cstr] in
     let base = beta_appvect (lift nargs p) (Array.of_list cargs) in
     it_mkProd_or_LetIn base args in
   Array.mapi build_one_branch mip.mind_nf_lc
 
 (* [p] is the predicate, [c] is the match object, [realargs] is the
    list of real args of the inductive type *)
-let build_case_type dep p c realargs =
-  let args = if dep then realargs@[c] else realargs in
-  beta_appvect p (Array.of_list args)
+let build_case_type p c realargs =
+  beta_appvect p (Array.of_list (realargs@[c]))
 
 let type_case_branches env (ind,largs) pj c =
   let specif = lookup_mind_specif env ind in 
   let nparams = inductive_params specif in
   let (params,realargs) = list_chop nparams largs in
   let p = pj.uj_val in
-  let (dep,univ) = is_correct_arity env c pj ind specif params in
-  let lc = build_branches_type ind specif params dep p in
-  let ty = build_case_type dep p c realargs in
+  let univ = is_correct_arity env c pj ind specif params in
+  let lc = build_branches_type ind specif params p in
+  let ty = build_case_type p c realargs in
   (lc, ty, univ)
 
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index d09cdbdb79..f877b5391f 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -65,6 +65,10 @@ val type_case_branches :
   env -> inductive * constr list -> unsafe_judgment -> constr
     -> types array * types * constraints
 
+val build_branches_type :
+  inductive -> mutual_inductive_body * one_inductive_body ->
+    constr list -> constr -> types array
+
 (* Return the arity of an inductive type *)
 val mind_arity : one_inductive_body -> rel_context * sorts_family