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

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

4 files changed, 36 insertions, 28 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 56660cd69f..4d1cefe5a5 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -335,17 +335,25 @@ let discharge_Function (_,finfos) =
 	 }
 
 open Term
+
+let pr_ocst c =
+  Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ())
+
 let pr_info f_info =
-  str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
-    str "function_constant_type := " ++
-    (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
-    str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
-    str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
-    str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
-    str "rect_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
-    str "rec_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
-    str "prop_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
-    str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
+  str "function_constant := " ++
+  Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
+  str "function_constant_type := " ++
+  (try
+     Printer.pr_lconstr
+       (Global.type_of_global (ConstRef f_info.function_constant))
+   with e when Errors.noncritical e -> mt ()) ++ fnl () ++
+  str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
+  str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
+  str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++
+  str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++
+  str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++
+  str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++
+  str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
 
 let pr_table tb =
   let l = Cmap.fold (fun k v acc -> v::acc) tb [] in
@@ -486,22 +494,17 @@ exception Building_graph of exn
 exception Defining_principle of exn
 exception ToShow of exn
 
-let init_constant dir s =
-  try
-    Coqlib.gen_constant "Function" dir s
-  with e -> raise (ToShow e)
-
 let jmeq () =
   try
-    (Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
-     init_constant ["Logic";"JMeq"] "JMeq")
-  with e -> raise (ToShow e)
+    Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
+    Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq"
+  with e when Errors.noncritical e -> raise (ToShow e)
 
 let jmeq_refl () =
   try
     Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
-    init_constant ["Logic";"JMeq"] "JMeq_refl"
-  with e -> raise (ToShow e)
+    Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl"
+  with e when Errors.noncritical e -> raise (ToShow e)
 
 let h_intros l =
   tclMAP h_intro l
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index bb775d40a4..16b1881f47 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -60,9 +60,13 @@ let observe strm =
 
 
 let do_observe_tac s tac g =
-  let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
+  let goal =
+    try Printer.pr_goal g
+    with e when Errors.noncritical e -> assert false
+  in
   try
-    let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
+    let v = tac g in
+    msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
   with reraise ->
     let e = Cerrors.process_vernac_interp_error reraise in
     msgnl (str "observation "++ s++str " raised exception " ++
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 97512dd846..bf5eba63a3 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -786,10 +786,10 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
 
   let params1 =
     try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
-    with _ -> [] in
+    with e when Errors.noncritical e -> [] in
   let params2 =
     try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
-    with _ -> [] in
+    with e when Errors.noncritical e -> [] in
 
   let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
   let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8a4cdc3c72..597233d01b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -423,7 +423,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	try
 	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info
-	with _ -> 
+	with e when Errors.noncritical e ->
 	  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Lambda(n,t,b) -> 
@@ -431,7 +431,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	try
 	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info
-	with _ -> 
+	with e when Errors.noncritical e ->
 	  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Case(ci,t,a,l) -> 
@@ -1240,8 +1240,9 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
   let name = match goal_name with
     | Some s -> s
     | None   ->
-	try (add_suffix current_proof_name "_subproof")
-	with _ -> anomaly (Pp.str "open_new_goal with an unamed theorem")
+	try add_suffix current_proof_name "_subproof"
+	with e when Errors.noncritical e ->
+          anomaly (Pp.str "open_new_goal with an unamed theorem")
   in
   let sign = initialize_named_context_for_proof () in
   let na = next_global_ident_away name [] in