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

7 files changed, 76 insertions, 30 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 7904c88ee..74780a8d2 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -41,7 +41,7 @@ let absurd c = Proofview.V82.tactic (absurd c)
 
 let filter_hyp f tac =
   let rec seek = function
-    | [] -> raise Not_found
+    | [] -> Proofview.tclZERO Not_found
     | (id,_,t)::rest when f t -> tac id
     | _::rest -> seek rest in
   Proofview.Goal.hyps >>= fun hyps ->
@@ -68,7 +68,8 @@ let contradiction_context =
 	           | Not_found -> seek_neg rest
                    | e -> Proofview.tclZERO e
                  end)
-	  | _ -> seek_neg rest in
+	  | _ -> seek_neg rest
+  in
   Proofview.Goal.hyps >>= fun hyps ->
   let hyps = Environ.named_context_of_val hyps in
   seek_neg hyps
@@ -82,6 +83,7 @@ let contradiction_term (c,lbind as cl) =
   Proofview.tclEVARMAP >= fun sigma ->
   Proofview.Goal.env >>= fun env ->
   Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+  try (* type_of can raise exceptions. *)
   let typ = type_of c in
   let _, ccl = splay_prod env sigma typ in
   if is_empty_type ccl then
@@ -99,6 +101,7 @@ let contradiction_term (c,lbind as cl) =
         | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
         | e -> Proofview.tclZERO e
       end
+  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 
 let contradiction = function
   | None -> Tacticals.New.tclTHEN intros contradiction_context
diff --git a/tactics/elim.ml b/tactics/elim.ml
index f8f85ef3c..b9f077aa4 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -87,6 +87,7 @@ let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c =
   Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+  try (* type_of can raise exceptions *)
   let typc = type_of c in
   Tacticals.New.tclTHENS (Proofview.V82.tactic (cut typc))
     [ Tacticals.New.tclTHEN (intro_using tmphyp_name)
@@ -94,6 +95,7 @@ let general_decompose recognizer c =
 	    (Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer)
 	      (fun id -> Proofview.V82.tactic (clear [id]))));
        Proofview.V82.tactic (exact_no_check c) ]
+  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 
 let head_in =
   Goal.env >- fun env ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e9fe23e56..ff35b4eeb 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -467,9 +467,11 @@ let general_multi_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
     Proofview.tclEVARMAP >= fun sigma ->
     Proofview.Goal.env >>= fun env ->
-    let sigma,c = f env sigma in
-    Tacticals.New.tclWITHHOLES with_evars
-      (general_multi_rewrite l2r with_evars ?tac c) sigma cl in
+    try (* f (an interpretation function) can raise exceptions *)
+      let sigma,c = f env sigma in
+      Tacticals.New.tclWITHHOLES with_evars
+        (general_multi_rewrite l2r with_evars ?tac c) sigma cl 
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in
   let rec doN l2r c = function
     | Precisely n when n <= 0 -> Proofview.tclUNIT ()
     | Precisely 1 -> do1 l2r c
@@ -859,17 +861,20 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
 let onEquality with_evars tac (c,lbindc) =
   Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
   Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
+  try (* type_of can raise exceptions *)
   let t = type_of c in
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
-  Tacmach.New.of_old make_clenv_binding >>= fun make_clenv_binding ->
-  let eq_clause = make_clenv_binding (c,t') lbindc in
+  Tacmach.New.of_old (fun gl -> make_clenv_binding gl (c,t') lbindc) >>= fun eq_clause ->
+  begin try (* clenv_pose_dependent_evars can raise exceptions *)
   let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
-  Tacmach.New.of_old find_this_eq_data_decompose >>= fun find_this_eq_data_decompose ->
-  let eq,eq_args = find_this_eq_data_decompose eqn in
+  Tacmach.New.of_old (fun gl -> find_this_eq_data_decompose gl eqn) >>= fun (eq,eq_args) ->
   Tacticals.New.tclTHEN
     (Proofview.V82.tactic (Refiner.tclEVARS eq_clause'.evd))
     (tac (eq,eqn,eq_args) eq_clause')
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
+  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 
 let onNegatedEquality with_evars tac =
   Proofview.tclEVARMAP >= fun sigma ->
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 8e551d3f3..e4d4fc80e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -449,12 +449,13 @@ let raw_inversion inv_kind id status names =
   let c = mkVar id in
   Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind >>= fun reduce_to_atomic_ind ->
   Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
-  let (ind,t) =
+  begin
     try
-      reduce_to_atomic_ind (type_of c)
+      Proofview.tclUNIT (reduce_to_atomic_ind (type_of c))
     with UserError _ ->
-      errorlabstrm "raw_inversion"
-	(str ("The type of "^(Id.to_string id)^" is not inductive.")) in
+      Proofview.tclZERO (Errors.UserError ("raw_inversion" ,
+	str ("The type of "^(Id.to_string id)^" is not inductive.")))
+  end >= fun (ind,t) ->
   Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>= fun indclause ->
   let ccl = clenv_type indclause in
   check_no_metas indclause ccl;
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1c5903d51..73fb292ed 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1668,7 +1668,10 @@ and interp_atomic ist tac =
       Tacmach.New.of_old (fun gl -> interp_intro_pattern_list_as_list ist gl l) >>= fun patterns ->
       h_intro_patterns patterns
   | TacIntrosUntil hyp ->
-      h_intros_until (interp_quantified_hypothesis ist hyp)
+      begin try (* interp_quantified_hypothesis can raise an exception *)
+        h_intros_until (interp_quantified_hypothesis ist hyp)
+      with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+      end
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.env >>= fun env ->
       Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>= fun mloc ->
@@ -1701,6 +1704,7 @@ and interp_atomic ist tac =
   | TacApply (a,ev,cb,cl) ->
       Proofview.tclEVARMAP >= fun sigma ->
       Proofview.Goal.env >>= fun env ->
+      begin try (* interp_open_constr_with_bindings_loc can raise exceptions *)
       let sigma, l =
         List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
       in
@@ -1711,12 +1715,17 @@ and interp_atomic ist tac =
               Tacmach.New.of_old (fun gl -> interp_in_hyp_as ist gl cl) >>= fun cl ->
               h_apply_in a ev l cl) in
       Tacticals.New.tclWITHHOLES ev tac sigma l
+      with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+      end
   | TacElim (ev,cb,cbo) ->
       Proofview.tclEVARMAP >= fun sigma ->
       Proofview.Goal.env >>= fun env ->
-      let sigma, cb = interp_constr_with_bindings ist env sigma cb in
-      let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
-      Tacticals.New.tclWITHHOLES ev (h_elim ev cb) sigma cbo
+      begin try (* interpretation functions may raise exceptions *)
+              let sigma, cb = interp_constr_with_bindings ist env sigma cb in
+              let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
+              Tacticals.New.tclWITHHOLES ev (h_elim ev cb) sigma cbo
+        with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+      end
   | TacElimType c ->
       Proofview.V82.tactic begin fun gl -> 
         let (sigma,c_interp) = pf_interp_type ist gl c in
@@ -1789,12 +1798,15 @@ and interp_atomic ist tac =
   | TacAssert (t,ipat,c) ->
       Proofview.tclEVARMAP >= fun sigma ->
       Proofview.Goal.env >>= fun env ->
-      let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in
-      Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>= fun patt ->
-      Tacticals.New.tclTHEN
-	(Proofview.V82.tactic (tclEVARS sigma))
-        (Tactics.forward (Option.map (interp_tactic ist) t)
-	   (Option.map patt ipat) c)
+      begin try (* intrerpreation function may raise exceptions *)
+              let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in
+              Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>= fun patt ->
+              Tacticals.New.tclTHEN
+	        (Proofview.V82.tactic (tclEVARS sigma))
+                (Tactics.forward (Option.map (interp_tactic ist) t)
+	           (Option.map patt ipat) c)
+        with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+      end
   | TacGeneralize cl ->
       Proofview.tclEVARMAP >= fun sigma ->
       Proofview.Goal.env >>= fun env ->
@@ -1822,8 +1834,11 @@ and interp_atomic ist tac =
           (h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
       else
         (* We try to keep the pattern structure as much as possible *)
-        h_let_pat_tac b (interp_fresh_name ist env na)
-          (interp_pure_open_constr ist env sigma c) clp eqpat
+        begin try
+          h_let_pat_tac b (interp_fresh_name ist env na)
+            (interp_pure_open_constr ist env sigma c) clp eqpat
+          with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+        end
 
   (* Automation tactics *)
   | TacTrivial (debug,lems,l) ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index b2405122e..816415b48 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -570,7 +570,10 @@ module New = struct
     (* applying elimination_scheme just a little modified *)
     let indclause' = clenv_match_args indbindings indclause in
     Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
-    Tacmach.New.of_old (fun gl -> mk_clenv_from gl (elim,type_of elim)) >>= fun elimclause ->
+    begin try (* type_of can raise an exception *)
+            Tacmach.New.of_old (fun gl -> mk_clenv_from gl (elim,type_of elim))
+      with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    end >>= fun elimclause ->
     let indmv =
       match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4026b4258..f6983cba3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1283,6 +1283,7 @@ let check_number_of_constructors expctdnumopt i nconstr =
 let constructor_tac with_evars expctdnumopt i lbind =
   Proofview.Goal.concl >>= fun cl ->
   Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
+  try (* reduce_to_quantified_ind can raise an exception *)
   let (mind,redcl) = reduce_to_quantified_ind cl in
   let nconstr =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
@@ -1291,6 +1292,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
   let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in
   (Tacticals.New.tclTHENLIST
      [Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
+  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 
 let one_constructor i lbind = constructor_tac false None i lbind
 
@@ -1303,6 +1305,7 @@ let any_constructor with_evars tacopt =
   let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
   Proofview.Goal.concl >>= fun cl ->
   Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
+  try (* reduce_to_quantified_ind can raise an exception *)
   let mind = fst (reduce_to_quantified_ind cl) in
   let nconstr =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
@@ -1311,6 +1314,7 @@ let any_constructor with_evars tacopt =
     (List.map
       (fun i -> Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t)
       (List.interval 1 nconstr))
+  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 
 let left_with_bindings  with_evars = constructor_tac with_evars (Some 2) 1
 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2
@@ -1399,6 +1403,7 @@ let rewrite_hyp l2r id =
   Proofview.Goal.env >>= fun env ->
   Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
   Tacmach.New.pf_apply whd_betadeltaiota >>= fun whd_betadeltaiota ->
+  try (* type_of can raise an exception *)
   let t = whd_betadeltaiota (type_of (mkVar id)) in
   (* TODO: detect setoid equality? better detect the different equalities *)
   match match_with_equality_type t with
@@ -1417,6 +1422,7 @@ let rewrite_hyp l2r id =
 	Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
   | _ ->
       Proofview.tclZERO (Errors.UserError ("",Pp.str"Cannot find a known equation."))
+  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 
 let rec explicit_intro_names = function
 | (_, IntroIdentifier id) :: l ->
@@ -1947,8 +1953,11 @@ let forward usetac ipat c =
   match usetac with
   | None ->
       Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
-      let t = type_of c in
-      Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c))
+      begin try (* type_of can raise an exception *)
+              let t = type_of c in
+              Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c))
+        with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+      end
   | Some tac ->
       Tacticals.New.tclTHENFIRST (assert_as true ipat c) tac
 
@@ -2146,6 +2155,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
 let atomize_param_of_ind (indref,nparams,_) hyp0 =
   Tacmach.New.pf_get_hyp_typ hyp0 >>= fun tmptyp0 ->
   Tacmach.New.pf_apply reduce_to_quantified_ref >>= fun reduce_to_quantified_ref ->
+  try (* reduce_to_quantified_ref can raise an exception *)
   let typ0 =  reduce_to_quantified_ref indref tmptyp0 in
   let prods, indtyp = decompose_prod typ0 in
   let argl = snd (decompose_app indtyp) in
@@ -2181,6 +2191,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
       Proofview.tclUNIT ()
   in
   atomize_one (List.length argl) params
+  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 
 let find_atomic_param_of_ind nparams indtyp =
   let argl = snd (decompose_app indtyp) in
@@ -3193,6 +3204,7 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n
   inhyps =
   Tacmach.New.pf_get_hyp_typ hyp0 >>= fun tmptyp0 ->
   Tacmach.New.pf_apply reduce_to_quantified_ref >>= fun reduce_to_quantified_ref ->
+  try (* reduce_to_quantified_ref can raise an exception *)
   let typ0 = reduce_to_quantified_ref indref tmptyp0 in
   let indvars = find_atomic_param_of_ind nparams ((strip_prod typ0)) in
   let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [
@@ -3202,6 +3214,7 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n
   ]) in
   apply_induction_in_context
     (Some (hyp0,inhyps)) elim indvars names induct_tac
+  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 
 let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps =
   Tacmach.New.of_old (find_induction_type isrec elim hyp0) >>= fun elim_info ->
@@ -3307,7 +3320,8 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
 
 	    | _ ->
                 Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
-		let x =
+		try (* type_of can raise an exception *)
+                let x =
 		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
 
                 Tacmach.New.of_old (fresh_id [] x) >>= fun id ->
@@ -3316,7 +3330,8 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
 		let _ = letids:=id::!letids in
 		Tacticals.New.tclTHEN
 		  (letin_tac None (Name id) c None allHypsAndConcl)
-		  (atomize_list newl') in
+		  (atomize_list newl')
+                with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in
   Tacticals.New.tclTHENLIST
     [
       (atomize_list lc);
@@ -3610,6 +3625,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 let symmetry_in id =
   Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+  try (* type_of can raise an exception *)
   let ctype = type_of (mkVar id) in
   let sign,t = decompose_prod_assum ctype in
   Proofview.tclORELSE
@@ -3627,6 +3643,7 @@ let symmetry_in id =
       | NoEquationFound -> Hook.get forward_setoid_symmetry_in id
       | e -> Proofview.tclZERO e
     end
+  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 
 let intros_symmetry =
   Tacticals.New.onClause