Restrict (try...with...) to avoid catching critical exn (part 10)

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

7 files changed, 85 insertions, 67 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index cae417ad36..38a616ddef 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -69,12 +69,13 @@ let _ =
       Summary.unfreeze_function = unfreeze;
       Summary.init_function     = init }
 
+let raw_find_base bas = String.Map.find bas !rewtab
+
 let find_base bas =
- try String.Map.find bas !rewtab
- with
-  Not_found ->
-   errorlabstrm "AutoRewrite"
-     (str ("Rewriting base "^(bas)^" does not exist."))
+  try raw_find_base bas
+  with Not_found ->
+    errorlabstrm "AutoRewrite"
+      (str ("Rewriting base "^(bas)^" does not exist."))
 
 let find_rewrites bas =
   List.rev_map snd (HintDN.find_all (find_base bas))
@@ -204,8 +205,9 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl =
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
-  let base = try find_base rbase with _ -> HintDN.empty in
-  let max = try fst (Util.List.last (HintDN.find_all base)) with _ -> 0 in
+  let base = try raw_find_base rbase with Not_found -> HintDN.empty in
+  let max = try fst (Util.List.last (HintDN.find_all base)) with Failure _ -> 0
+  in
   let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
     rewtab:=String.Map.add rbase (HintDN.union lrl base) !rewtab
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 29429d01dc..8ed4ab1fc1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -333,7 +333,8 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
 	  try
 	    rewrite_side_tac (!general_rewrite_clause cls
 				 lft2rgt occs (c,l) ~new_goals:[]) tac gl
-	  with e -> (* Try to see if there's an equality hidden *)
+	  with e when Errors.noncritical e ->
+            (* Try to see if there's an equality hidden *)
             let e = Errors.push e in
 	    let env' = push_rel_context rels env in
 	    let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
@@ -1155,7 +1156,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
         (* not a dep eq or no decidable type found *)
         end
         else raise Not_dep_pair
-      with e ->
+      with e when Errors.noncritical e ->
 	inject_at_positions env sigma u eq_clause posns
 	  (fun _ -> intros_pattern MoveLast ipats)
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index a4f7b5e3fa..c99c15a458 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -490,7 +490,7 @@ let wrap_inv_error id = function
 (* The most general inversion tactic *)
 let inversion inv_kind status names id gls =
   try (raw_inversion inv_kind id status names) gls
-  with e -> wrap_inv_error id e
+  with e when Errors.noncritical e -> wrap_inv_error id e
 
 (* Specializing it... *)
 
@@ -533,7 +533,7 @@ let invIn k names ids id gls =
        inversion (false,k) NoDep names id;
        intros_replace_ids])
     gls
-  with e -> wrap_inv_error id e
+  with e when Errors.noncritical e -> wrap_inv_error id e
 
 let invIn_gen k names idl = try_intros_until (invIn k names idl)
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index d3c9e6bb6a..db2c19f006 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -442,13 +442,13 @@ let dump_glob_red_expr = function
     try
       Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
 	(Smartlocate.smart_global r)
-    with _ -> ()) occs
+    with e when Errors.noncritical e -> ()) occs
   | Cbv grf | Lazy grf ->
     List.iter (fun r ->
       try
         Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
 	  (Smartlocate.smart_global r)
-      with _ -> ()) grf.rConst
+      with e when Errors.noncritical e -> ()) grf.rConst
   | _ -> ()
 
 let intern_red_expr ist = function
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 274a235599..e52d784114 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -44,7 +44,7 @@ open Tacintern
 
 let safe_msgnl s =
   let _ =
-    try ppnl s with e ->
+    try ppnl s with any ->
     ppnl (str "bug in the debugger: an exception is raised while printing debug information")
   in
   pp_flush () 
@@ -69,7 +69,7 @@ type value =
 let dloc = Loc.ghost
 
 let catch_error call_trace tac g =
-  try tac g with e ->
+  try tac g with e when Errors.noncritical e ->
   let e = Errors.push e in
   let inner_trace,loc,e = match e with
   | LtacLocated (inner_trace,loc,e) -> inner_trace,loc,e
@@ -625,21 +625,22 @@ let interp_may_eval f ist gl = function
   | ConstrTerm c ->
      try
 	f ist gl c
-     with e ->
-       let e = Errors.push e in
-       debugging_exception_step ist false e (fun () ->
+     with reraise ->
+       let reraise = Errors.push reraise in
+       debugging_exception_step ist false reraise (fun () ->
          str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c));
-       raise e
+       raise reraise
 
 (* Interprets a constr expression possibly to first evaluate *)
 let interp_constr_may_eval ist gl c =
   let (sigma,csr) =
     try
       interp_may_eval pf_interp_constr ist gl c
-    with e ->
-      let e = Errors.push e in
-      debugging_exception_step ist false e (fun () -> str"evaluation of term");
-      raise e
+    with reraise ->
+      let reraise = Errors.push reraise in
+      debugging_exception_step ist false reraise
+        (fun () -> str"evaluation of term");
+      raise reraise
   in
   begin
     db_constr ist.debug (pf_env gl) csr;
@@ -1150,10 +1151,12 @@ and interp_app loc ist gl fv largs =
 	    try
               catch_error trace
 		(val_interp {ist with lfun=newlfun@olfun; trace=[]} gl) body
-	    with e ->
-              let e = Errors.push e in
-              debugging_exception_step ist false e (fun () -> str "evaluation");
-	      raise e in
+	    with reraise ->
+              let reraise = Errors.push reraise in
+              debugging_exception_step ist false reraise
+                (fun () -> str "evaluation");
+	      raise reraise
+          in
           (* No errors happened, we propagate the trace *)
           let v = append_trace trace v in
 
@@ -1193,16 +1196,14 @@ and eval_with_fail ist is_lazy goal tac =
 	let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in
 	VRTactic (catch_error trace tac { goal with sigma=sigma })
     | a -> a)
-  with e ->
+  with
     (** FIXME: Should we add [Errors.push]? *)
-    match e with
     | FailError (0,s) | LtacLocated (_,_,FailError (0,s)) ->
 	raise (Eval_fail (Lazy.force s))
-    | FailError (lvl,s) ->
-      raise (Exninfo.copy e (FailError (lvl - 1, s)))
+    | FailError (lvl,s) as e ->
+        raise (Exninfo.copy e (FailError (lvl - 1, s)))
     | LtacLocated (s'',loc,FailError (lvl,s')) ->
 	raise (LtacLocated (s'',loc,FailError (lvl - 1, s')))
-    | _ -> raise e
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist gl llc u =
@@ -1446,21 +1447,22 @@ and interp_match ist g lz constr lmr =
         (try
             let lmatch =
               try extended_matches c csr
-              with e ->
-                let e = Errors.push e in
-                debugging_exception_step ist false e (fun () ->
+              with reraise ->
+                let reraise = Errors.push reraise in
+                debugging_exception_step ist false reraise (fun () ->
                   str "matching with pattern" ++ fnl () ++
                   pr_constr_pattern_env (pf_env g) c);
-                raise e in
+                raise reraise
+            in
             try
               let lfun = extend_values_with_bindings lmatch ist.lfun in
               eval_with_fail { ist with lfun=lfun } lz g mt
-            with e ->
-              let e = Errors.push e in
-              debugging_exception_step ist false e (fun () ->
+            with reraise ->
+              let reraise = Errors.push reraise in
+              debugging_exception_step ist false reraise (fun () ->
                 str "rule body for pattern" ++
                 pr_constr_pattern_env (pf_env g) c);
-              raise e
+              raise reraise
          with e when is_match_catchable e ->
            debugging_step ist (fun () -> str "switching to the next rule");
            apply_match ist sigma csr tl)
@@ -1472,17 +1474,22 @@ and interp_match ist g lz constr lmr =
       errorlabstrm "Tacinterp.apply_match" (str
         "No matching clauses for match.") in
   let (sigma,csr) =
-      try interp_ltac_constr ist g constr with e ->
-       let e = Errors.push e in
-        debugging_exception_step ist true e
+      try interp_ltac_constr ist g constr
+      with reraise ->
+       let reraise = Errors.push reraise in
+        debugging_exception_step ist true reraise
           (fun () -> str "evaluation of the matched expression");
-        raise e in
+        raise reraise
+  in
   let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) sigma lmr in
   let res =
-     try apply_match ist sigma csr ilr with e ->
-       let e = Errors.push e in
-       debugging_exception_step ist true e (fun () -> str "match expression");
-       raise e in
+     try apply_match ist sigma csr ilr
+     with reraise ->
+       let reraise = Errors.push reraise in
+       debugging_exception_step ist true reraise
+         (fun () -> str "match expression");
+       raise reraise
+  in
   debugging_step ist (fun () ->
     str "match expression returns " ++ pr_value (Some (pf_env g)) (snd res));
   res
@@ -1982,7 +1989,7 @@ let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t))
 let tacticIn t =
   globTacticIn (fun ist ->
     try glob_tactic (t ist)
-    with e -> anomaly ~label:"tacticIn"
+    with e when Errors.noncritical e -> anomaly ~label:"tacticIn"
       (str "Incorrect tactic expression. Received exception is:" ++
        Errors.print e))
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a3733b3e77..3def7a48ad 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1039,9 +1039,10 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
   let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
-    with err ->
+    with e when Errors.noncritical e ->
     try aux (clenv_push_prod clause)
-    with NotExtensibleClause -> raise err in
+    with NotExtensibleClause -> raise e
+  in
   aux (make_clenv_binding gl (d,thm) lbind)
 
 let apply_in_once sidecond_first with_delta with_destruct with_evars id
@@ -1730,7 +1731,7 @@ let make_pattern_test env sigma0 (sigma,c) =
   let flags = default_matching_flags sigma0 in
   let matching_fun t =
     try let sigma = w_unify env sigma Reduction.CONV ~flags c t in Some(sigma,t)
-    with _ -> raise NotUnifiable in
+    with e when Errors.noncritical e -> raise NotUnifiable in
   let merge_fun c1 c2 =
     match c1, c2 with
     | Some (_,c1), Some (_,c2) when not (is_fconv Reduction.CONV env sigma0 c1 c2) ->
@@ -2578,8 +2579,11 @@ let specialize_eqs id gl =
       
 
 let specialize_eqs id gl =
-  if try ignore(clear [id] gl); false with _ -> true then
-    tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl 
+  if
+    (try ignore(clear [id] gl); false
+     with e when Errors.noncritical e -> true)
+  then
+    tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl
   else specialize_eqs id gl
 
 let occur_rel n c =
@@ -2739,7 +2743,8 @@ let compute_elim_sig ?elimc elimt =
       | Some ( _,None,ind) ->
 	  let indhd,indargs = decompose_app ind in
 	  try {!res with indref = Some (global_of_constr indhd) }
-	  with _ -> error "Cannot find the inductive type of the inductive scheme.";;
+	  with e when Errors.noncritical e ->
+            error "Cannot find the inductive type of the inductive scheme.";;
 
 let compute_scheme_signature scheme names_info ind_type_guess =
   let f,l = decompose_app scheme.concl in
@@ -3579,4 +3584,4 @@ let unify ?(state=full_transparent_state) x y gl =
     in
     let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y
     in tclEVARS evd gl
-  with _ -> tclFAIL 0 (str"Not unifiable") gl
+  with e when Errors.noncritical e -> tclFAIL 0 (str"Not unifiable") gl
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 3fa932f063..31d03ff0c4 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -106,7 +106,7 @@ let mkFullInd ind n =
 
 let check_bool_is_defined () =
   try let _ = Global.type_of_global Coqlib.glob_bool in ()
-  with _ -> raise (UndefinedCst "bool")
+  with e when Errors.noncritical e -> raise (UndefinedCst "bool")
 
 let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
@@ -299,7 +299,7 @@ let destruct_ind c =
     try let u,v =  destApp c in
           let indc = destInd u in
             indc,v
-    with _-> let indc = destInd c in
+    with DestKO -> let indc = destInd c in
             indc,[||]
 
 (*
@@ -324,7 +324,8 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q =
             else error ("Var "^(Id.to_string s)^" seems unknown.")
       )
     in mkVar (find 1)
-  with _ -> (* if this happen then the args have to be already declared as a
+  with e when Errors.noncritical e ->
+      (* if this happen then the args have to be already declared as a
               Parameter*)
       (
         let mp,dir,lbl = repr_con (destConst v) in
@@ -371,8 +372,9 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
             else error ("Var "^(Id.to_string s)^" seems unknown.")
       )
     in mkVar (find 1)
-  with _ -> (* if this happen then the args have to be already declared as a
-              Parameter*)
+  with e when Errors.noncritical e ->
+      (* if this happen then the args have to be already declared as a
+         Parameter*)
       (
         let mp,dir,lbl = repr_con (destConst v) in
           mkConst (make_con mp dir (Label.make (
@@ -389,7 +391,7 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
         else (
           let u,v = try  destruct_ind tt1
           (* trick so that the good sequence is returned*)
-                with _ -> ind,[||]
+                with e when Errors.noncritical e -> ind,[||]
           in if eq_ind u ind
              then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2)
              else (
@@ -423,15 +425,15 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
     | _ -> error "Both side of the equality must have the same arity."
   in
   let (ind1,ca1) = try destApp lft with
-    _ -> error "replace failed."
+    DestKO -> error "replace failed."
   and (ind2,ca2) = try destApp rgt with
-    _ -> error "replace failed."
+    DestKO -> error "replace failed."
   in
   let (sp1,i1) = try destInd ind1 with
-    _ -> (try fst (destConstruct ind1) with _ ->
+    DestKO -> (try fst (destConstruct ind1) with _ ->
                 error "The expected type is an inductive one.")
   and (sp2,i2) = try destInd ind2 with
-    _ -> (try fst (destConstruct ind2)  with _ ->
+    DestKO -> (try fst (destConstruct ind2)  with _ ->
                 error "The expected type is an inductive one.")
   in
     if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
@@ -709,7 +711,8 @@ let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind
 (* Decidable equality *)
 
 let check_not_is_defined () =
-  try ignore (Coqlib.build_coq_not ()) with _ -> raise (UndefinedCst "not")
+  try ignore (Coqlib.build_coq_not ())
+  with e when Errors.noncritical e -> raise (UndefinedCst "not")
 
 (* {n=m}+{n<>m}  part  *)
 let compute_dec_goal ind lnamesparrec nparrec =