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

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

5 files changed, 23 insertions, 13 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 329be18eb1..123b2a2efd 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -690,7 +690,7 @@ let resolve_typeclass_evars debug m env evd filter split fail =
   let evd = 
     try Evarconv.consider_remaining_unif_problems
       ~ts:(Typeclasses.classes_transparent_state ()) env evd
-    with _ -> evd
+    with e when Errors.noncritical e -> evd
   in
     resolve_all_evars debug m env (initial_select_evars filter) evd split fail
 
@@ -780,7 +780,11 @@ END
 
 let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl =
   try 
-    let dbs = List.map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
+    let dbs = List.map_filter
+      (fun db -> try Some (Auto.searchtable_map db)
+        with e when Errors.noncritical e -> None)
+      dbs
+    in
     let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
       eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl
    with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index caebb76d4c..1be29aefe6 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -197,7 +197,8 @@ module SearchProblem = struct
 (* 	    let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
 (* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
 	      (lgls,pptac) :: aux tacl
-	  with e -> Refiner.catch_failerror e; aux tacl
+	  with e when Errors.noncritical e ->
+            Refiner.catch_failerror e; aux tacl
     in aux l
 
   (* Ordering of states is lexicographic on depth (greatest first) then
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 7a8cccc6d7..a8188d5820 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -611,7 +611,7 @@ let hResolve_auto id c t gl =
       hResolve id c n t gl
     with
     | UserError _ as e -> raise e
-    | _ -> resolve_auto (n+1)
+    | e when Errors.noncritical e -> resolve_auto (n+1)
   in
   resolve_auto 1
 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index fadc50661a..286aa94929 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -366,7 +366,10 @@ let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
 let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ]
 
 let match_eq eqn eq_pat =
-  let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in
+  let pat =
+    try Lazy.force eq_pat
+    with e when Errors.noncritical e -> raise PatternMatchingFailure
+  in
   match matches pat eqn with
     | [(m1,t);(m2,x);(m3,y)] ->
 	assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 20bcb84a75..a3006e99cc 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -118,7 +118,7 @@ let is_applied_rewrite_relation env sigma rels t =
 	      let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in
 	      let _ = Typeclasses.resolve_one_typeclass env' evd inst in
 		Some (it_mkProd_or_LetIn t rels)
-	  with _ -> None)
+	  with e when Errors.noncritical e -> None)
   | _ -> None
 
 let _ =
@@ -218,7 +218,7 @@ let cstrevars evars = snd evars
 
 let evd_convertible env evd x y =
   try ignore(Evarconv.the_conv_x env x y evd); true
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 let rec decompose_app_rel env evd t = 
   match kind_of_term t with
@@ -1040,7 +1040,8 @@ module Strategies =
 	let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in
 	let unfolded =
 	  try Tacred.try_red_product env sigma c
-	  with _ -> error "fold: the term is not unfoldable !"
+	  with e when Errors.noncritical e ->
+            error "fold: the term is not unfoldable !"
 	in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
@@ -1048,7 +1049,7 @@ module Strategies =
 	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
 			   rew_prf = RewCast DEFAULTcast; 
 			   rew_evars = sigma, cstrevars evars })
-	  with _ -> None
+	  with e when Errors.noncritical e -> None
 
     let fold_glob c : strategy =
       fun env avoid t ty cstr evars ->
@@ -1056,7 +1057,8 @@ module Strategies =
 	let sigma, c = Pretyping.understand_tcc (goalevars evars) env c in
 	let unfolded =
 	  try Tacred.try_red_product env sigma c
-	  with _ -> error "fold: the term is not unfoldable !"
+	  with e when Errors.noncritical e ->
+            error "fold: the term is not unfoldable !"
 	in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
@@ -1064,7 +1066,7 @@ module Strategies =
 	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
 			   rew_prf = RewCast DEFAULTcast; 
 			   rew_evars = sigma, cstrevars evars })
-	  with _ -> None
+	  with e when Errors.noncritical e -> None
   
 
 end
@@ -1306,7 +1308,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
   
 let newtactic_init_setoid () = 
   try init_setoid (); Proofview.tclUNIT ()
-  with e -> Proofview.tclZERO e
+  with e when Errors.noncritical e -> Proofview.tclZERO e
 
 let tactic_init_setoid () = 
   init_setoid (); tclIDTAC
@@ -1979,7 +1981,7 @@ let setoid_proof gl ty fn fallback =
       let evm = project gl in
       let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
 	fn env evm car rel gl
-    with e ->
+    with e when Errors.noncritical e ->
       try fallback gl
       with Hipattern.NoEquationFound ->
           let e = Errors.push e in