Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).

They were a hack to avoid looking where exceptions were raised and not
caught. Hopefully I produce a cleaner stack now, catching errors when
it is needed.

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

1 files changed, 4 insertions, 2 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index c4fa51c4b..3976fcf14 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -351,8 +351,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
         )))
       )
   in
-  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
-  let type_of_pq = type_of p in
+  Tacmach.New.of_old (fun gl -> pf_type_of gl p) >>= fun type_of_pq ->
     let u,v = destruct_ind type_of_pq
     in let lb_type_of_p =
         try
@@ -412,6 +411,7 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
     match (l1,l2) with
     | (t1::q1,t2::q2) ->
         Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+        begin try (* type_of can raise an exception *)
         let tt1 = type_of t1 in
         if eq_constr t1 t2 then aux q1 q2
         else (
@@ -452,6 +452,8 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
                   aux q1 q2 ]
               )
         )
+          with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+        end
     | ([],[]) -> Proofview.tclUNIT ()
     | _ -> Proofview.tclZERO (UserError ("" , str"Both side of the equality must have the same arity."))
   in