]> matita.cs.unibo.it Git - helm.git/commitdiff
added assertion (that is a TODO) in case non-considered exceptions are raised when...
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 25 Nov 2006 11:26:09 +0000 (11:26 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 25 Nov 2006 11:26:09 +0000 (11:26 +0000)
helm/software/components/cic_unification/cicRefine.ml

index 36347ccd1a4f2c5b30f51c2b43b984af3e3a7146..d10e177d02d61b3aa783353a5582fa134f06dad4 100644 (file)
@@ -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)->