It happens that the type inference algorithm (pretyping) did not check

that the return predicate of the match construction is at an allowed
sort, resulting in tactics possibly manipulating ill-typed terms. This
is now fixed,

Incidentally removed in pretyping an ill-placed coercion.

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

1 files changed, 4 insertions, 2 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 121d7dcc1..b104db026 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -947,7 +947,7 @@ let specialize_predicate newtomatchs (names,(depna,_)) arsign cs tms ccl =
   snd (List.fold_left (expand_arg tms) (1,ccl''') newtomatchs)
 
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
-  let pred= abstract_predicate env !evdref indf current dep tms p in
+  let pred = abstract_predicate env !evdref indf current dep tms p in
   (pred, whd_betaiota !evdref
            (applist (pred, realargs@[current])))
 
@@ -1169,7 +1169,9 @@ and match_current pb tomatch =
 	    find_predicate pb.caseloc pb.env pb.evdref
 	      pb.pred current indt (names,dep) pb.tomatch in
 	  let ci = make_case_info pb.env mind pb.casestyle in
-	  let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
+	  let pred = nf_betaiota !(pb.evdref) pred in
+	  let case = mkCase (ci,pred,current,brvals) in
+	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
 	    uj_type = substl inst typ }