Exception raised by delift changed:

[helm.git] / helm / ocaml / cic_proof_checking / cicSubstitution.ml

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 5f35c54b9d172bad15052cc423e07237f31cd408..229da24f0fdbdf7b5183c288fe1e8d5ac05937c9 100644 (file)
--- 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) ->