X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fdiscrimination_tree.ml;h=56e8bd44af404f5596fb6586e540e403c77af3dc;hb=86eaff4471bdce9f632838d3a0b18d082015c2db;hp=dc87e750398a9ea647c48683ad4f559e5bac8097;hpb=e701ae61ea78b5bcbc8919ccb51f4f2ada8c5f23;p=helm.git

diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml
index dc87e7503..56e8bd44a 100644
--- 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