From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 8 May 2013 17:47:10 +0200
Subject: Imported Upstream version 8.4pl2dfsg

---
 plugins/romega/const_omega.ml |  4 ++--
 plugins/romega/refl_omega.ml  | 30 ++++++++++++++++++------------
 2 files changed, 20 insertions(+), 14 deletions(-)

(limited to 'plugins/romega')

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index e810e15c..fb45e816 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -335,7 +335,7 @@ let parse_term t =
     | Kapp("Z.succ",[t]) -> Tsucc t
     | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) ->
-	(try Tnum (recognize t) with _ -> Tother)
+	(try Tnum (recognize t) with e when Errors.noncritical e -> Tother)
     | _ -> Tother
   with e when Logic.catchable_exception e -> Tother
 
@@ -357,6 +357,6 @@ let is_scalar t =
     | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true
     | _ -> false in
-  try aux t with _ -> false
+  try aux t with e when Errors.noncritical e -> false
 
 end
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 4a6d462e..e57230cb 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -225,7 +225,8 @@ let add_reified_atom t env =
     env.terms <- env.terms @ [t]; i
 
 let get_reified_atom env =
-  try List.nth env.terms with _ -> failwith "get_reified_atom"
+  try List.nth env.terms
+  with e when Errors.noncritical e -> failwith "get_reified_atom"
 
 (* \subsection{Gestion de l'environnement de proposition pour Omega} *)
 (* ajout d'une proposition *)
@@ -235,7 +236,9 @@ let add_prop env t =
     let i = List.length env.props in  env.props <- env.props @ [t]; i
 
 (* accès a une proposition *)
-let get_prop v env = try List.nth v env with _ -> failwith "get_prop"
+let get_prop v env =
+  try List.nth v env
+  with e when Errors.noncritical e -> failwith "get_prop"
 
 (* \subsection{Gestion du nommage des équations} *)
 (* Ajout d'une equation dans l'environnement de reification *)
@@ -247,7 +250,8 @@ let add_equation env e =
 (* accès a une equation *)
 let get_equation env id =
   try Hashtbl.find env.equations id
-  with e -> Printf.printf "Omega Equation %d non trouvée\n" id; raise e
+  with Not_found as e ->
+    Printf.printf "Omega Equation %d non trouvée\n" id; raise e
 
 (* Affichage des termes réifiés *)
 let rec oprint ch = function
@@ -349,7 +353,8 @@ let rec reified_of_formula env = function
       app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |]
 
 let reified_of_formula env f =
-  begin try reified_of_formula env f with e -> oprint stderr f; raise e end
+  try reified_of_formula env f
+  with reraise -> oprint stderr f; raise reraise
 
 let rec reified_of_proposition env = function
     Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) ->
@@ -380,8 +385,8 @@ let rec reified_of_proposition env = function
   | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |]
 
 let reified_of_proposition env f =
-  begin try reified_of_proposition env f
-  with e -> pprint stderr f; raise e end
+  try reified_of_proposition env f
+  with reraise -> pprint stderr f; raise reraise
 
 (* \subsection{Omega vers COQ réifié} *)
 
@@ -397,11 +402,11 @@ let reified_of_omega env body constant =
   List.fold_right mk_coeff body coeff_constant
 
 let reified_of_omega env body c  =
-  begin try
+  try
     reified_of_omega env body c
-  with e ->
-    display_eq display_omega_var (body,c); raise e
-  end
+  with reraise ->
+    display_eq display_omega_var (body,c); raise reraise
+
 
 (* \section{Opérations sur les équations}
 Ces fonctions préparent les traces utilisées par la tactique réfléchie
@@ -1000,10 +1005,11 @@ let rec solve_with_constraints all_solutions path =
   let weighted = filter_compatible_systems path all_solutions in
   let (winner_sol,winner_deps) =
     try select_smaller weighted
-    with e ->
+    with reraise ->
       Printf.printf "%d - %d\n"
 	(List.length weighted) (List.length all_solutions);
-      List.iter display_depend path; raise e in
+      List.iter display_depend path; raise reraise
+  in
   build_tree winner_sol (List.rev path) winner_deps
 
 let find_path {o_hyp=id;o_path=p} env =
-- 
cgit v1.2.3