X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=d10e177d02d61b3aa783353a5582fa134f06dad4;hb=0de62d69d01f334e0300633d22b63c91edd8fc7f;hp=36347ccd1a4f2c5b30f51c2b43b984af3e3a7146;hpb=7e30c63fcf9f9fe1780ba7aa4d95fd0d8658548b;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 36347ccd1..d10e177d0 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1386,7 +1386,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                         in
                         Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
                       with Uncertain _ | RefineFailure _ -> None
-                with Uncertain _ | RefineFailure _ -> None)
+                with Uncertain _ | RefineFailure _ -> None 
+                    | exn -> assert false) (* ritornare None, e' un localized *)
               candidates
            with
            | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->