- better exception handling

[helm.git] / helm / ocaml / paramodulation / discrimination_tree.ml

diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml
index dc87e750398a9ea647c48683ad4f559e5bac8097..56e8bd44af404f5596fb6586e540e403c77af3dc 100644 (file)
--- a/helm/ocaml/paramodulation/discrimination_tree.ml
+++ b/helm/ocaml/paramodulation/discrimination_tree.ml
@@ -145,7 +145,8 @@ let rec subterm_at_pos pos term =
   | index::pos ->
       match term with
       | Cic.Appl l ->
-          (try subterm_at_pos pos (List.nth l index) with _ -> raise Not_found)
+          (try subterm_at_pos pos (List.nth l index)
+           with Failure _ -> raise Not_found)
       | _ -> raise Not_found
 ;;
 
@@ -198,7 +199,7 @@ let retrieve_generalizations tree term =
         in
         try
           let n = PSMap.find (Cic.Implicit None) map in
-          let newpos = try after_t pos term with _ -> [-1] in
+          let newpos = try after_t pos term with Not_found -> [-1] in
           if newpos = [-1] then
             match n with
             | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res
@@ -264,7 +265,7 @@ let retrieve_unifiables tree term =
             in
             try
               let n = PSMap.find (Cic.Implicit None) map in
-              let newpos = try after_t pos term with _ -> [-1] in
+              let newpos = try after_t pos term with Not_found -> [-1] in
               if newpos = [-1] then
                 match n with
                 | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res