X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=7cf16ee53403f1d908c20984a3834d42f445e514;hb=3fec2330f2d30d47ebca0decd30bd2a457a9cbd3;hp=96b38e424970161afcbd301424eee55079f4adee;hpb=bf60fc57745fba8a2a22215ed1286eceae0f7700;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 96b38e424..7cf16ee53 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -504,14 +504,19 @@ let delift n subst context metasenv l t =
                     (*CSC: deliftato la regola per il LetIn                 *)
                     (*CSC: FALSO! La regola per il LetIn non lo fa          *)
          else
-          (match List.nth context (m-k-1) with
-            Some (_,C.Def (t,_)) ->
-             (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
-             (*CSC: first order unification. Does it help or does it harm? *)
-             deliftaux k (S.lift m t)
-          | Some (_,C.Decl t) ->
-             C.Rel ((position (m-k) l) + k)
-          | None -> raise (MetaSubstFailure "RelToHiddenHypothesis"))
+          (try
+            match List.nth context (m-k-1) with
+               Some (_,C.Def (t,_)) ->
+                (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
+                (*CSC: first order unification. Does it help or does it harm? *)
+                deliftaux k (S.lift m t)
+             | Some (_,C.Decl t) ->
+                C.Rel ((position (m-k) l) + k)
+             | None -> raise (MetaSubstFailure "RelToHiddenHypothesis")
+           with
+            Failure _ ->
+             raise (MetaSubstFailure "Unbound variable found in deliftaux")
+          )
      | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
@@ -593,7 +598,7 @@ let delift n subst context metasenv l t =
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
 debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
-print_endline "\nCicMetaSubst: UNCERTAIN" ;
+print_string "\nCicMetaSubst: UNCERTAIN" ;
       raise (Uncertain (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)