X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;fp=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=229da24f0fdbdf7b5183c288fe1e8d5ac05937c9;hb=47c9a0967ce271e551d4cbc8ac388097d774a3ef;hp=5f35c54b9d172bad15052cc423e07237f31cd408;hpb=4c1967e287c35d226e773df8d221293c3c74c9d4;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 5f35c54b9..229da24f0 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -29,6 +29,7 @@ exception ReferenceToVariable;;
 exception ReferenceToConstant;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
+exception DeliftingWouldCaptureAFreeVariable;;
 
 let debug_print = fun _ -> ()
 
@@ -117,7 +118,7 @@ let delift_from k n =
        if m < k then
         C.Rel m
        else if m < k + n then
-         (failwith "delifting this term whould capture free variables")
+         raise DeliftingWouldCaptureAFreeVariable
        else
         C.Rel (m - n)
     | C.Var (uri,exp_named_subst) ->