- Fixed bug #2021 (uncaught exception with injection/discriminate when

  the inductive status of a projectable position comes from a
  dependency).
- Improved doc of the stdlib chapter (see bug #2018), and fixed tex
  bugs introduced in r11725.
- Applied wish #2012 (max_dec transparent).



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

1 files changed, 8 insertions, 4 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index cdc096e84..259f51ad1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -457,8 +457,9 @@ let injectable env sigma t1 t2 =
 let descend_then sigma env head dirn =
   let IndType (indf,_) =
     try find_rectype env sigma (get_type_of env sigma head)
-    with Not_found -> assert false in
-  let ind,_ = dest_ind_family indf in
+    with Not_found ->
+      error "Cannot project on an inductive type derived from a dependency." in
+   let ind,_ = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
   let cstr = get_constructors env indf in
   let dirn_nlams = cstr.(dirn-1).cs_nargs in
@@ -477,7 +478,7 @@ let descend_then sigma env head dirn =
           (interval 1 (Array.length mip.mind_consnames)) in
       let ci = make_case_info env ind RegularStyle in
       mkCase (ci, p, head, Array.of_list brl)))
-  
+
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
 
@@ -828,11 +829,14 @@ let make_iterated_tuple env sigma dflt (z,zty) =
 let rec build_injrec sigma env dflt c = function
   | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c)
   | ((sp,cnum),argnum)::l ->
+    try
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
       let newc = mkRel(cnum_nlams-argnum) in
       let (subval,tuplety,dfltval) = build_injrec sigma cnum_env dflt newc l in
       (kont subval (dfltval,tuplety),
-       tuplety,dfltval)
+      tuplety,dfltval)
+    with
+	UserError _ -> failwith "caught"
 
 let build_injector sigma env dflt c cpath =
   let (injcode,resty,_) = build_injrec sigma env dflt c cpath in