From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 25 Nov 2006 11:26:09 +0000 (+0000)
Subject: added assertion (that is a TODO) in case non-considered exceptions are raised when... 
X-Git-Tag: 0.4.95@7852~785
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=70c533b5592b0bb91f544fec275213b866bf33ea;p=helm.git

added assertion (that is a TODO) in case non-considered exceptions are raised when tring to apply coercions
---

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 36347ccd1..d10e177d0 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/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)->