X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.ml;h=7fcd6a473f4595f70047f2bda5fce0b6867b68bf;hb=5c92c318030a05c766b3f6070dbd23589cbdee04;hp=28aa0adf0b4816dbd94837371b8bd8af7f4c9eea;hpb=668fb315dc8502dc1b4d336eba19ab9436bf5b7a;p=helm.git

diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
index 28aa0adf0..7fcd6a473 100644
--- a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
@@ -177,6 +177,7 @@ let fresh_uri status prefix suffix =
    diverge (mk "") 0
 ;;
 
+exception Stop;;
 
 let close_graph name t s d to_s from_d p a status =
   let c =
@@ -224,7 +225,7 @@ let close_graph name t s d to_s from_d p a status =
          let pos = 
            match p with 
            | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) 
-           | t -> assert false
+           | t -> raise Stop
          in
          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
          let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
@@ -251,7 +252,7 @@ let close_graph name t s d to_s from_d p a status =
        with 
        | NCicTypeChecker.TypeCheckerFailure _
        | NCicUnification.UnificationFailure _ 
-       | NCicUnification.Uncertain _ -> None
+       | NCicUnification.Uncertain _ | Stop -> None
      ) composites
   in
     composites