From 47c9a0967ce271e551d4cbc8ac388097d774a3ef Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 9 Jun 2005 13:41:22 +0000
Subject: [PATCH] Exception raised by delift changed: Failure ==>
 DeliftingWouldCaptureAFreeVariable

---
 helm/ocaml/cic_proof_checking/cicSubstitution.ml  | 3 ++-
 helm/ocaml/cic_proof_checking/cicSubstitution.mli | 1 +
 helm/ocaml/cic_unification/cicRefine.ml           | 4 ++--
 3 files changed, 5 insertions(+), 3 deletions(-)

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) ->
diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
index b1c09277b..5c8fa7ca5 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
@@ -28,6 +28,7 @@ exception RelToHiddenHypothesis;;
 exception ReferenceToVariable;;
 exception ReferenceToConstant;;
 exception ReferenceToInductiveDefinition;;
+exception DeliftingWouldCaptureAFreeVariable;;
 
 (* lift n t         *)
 (* lifts [t] of [n] *)
diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 53dea97e9..57e4c5e9d 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -529,7 +529,7 @@ and type_of_aux' metasenv context t ugraph =
                                    in
                                     candidate_oty,ugraph,metasenv,subst
                                  with
-                                    Failure _
+                                    CicSubstitution.DeliftingWouldCaptureAFreeVariable
                                   | CicUnification.UnificationFailure _
                                   | CicUnification.Uncertain _ ->
                                      None,ugraph,metasenv,subst
@@ -549,7 +549,7 @@ and type_of_aux' metasenv context t ugraph =
                            Some
                             (add_lambdas 0 t arity_instantiated_with_left_args),
                            ugraph,metasenv,subst
-                     with Failure s -> 
+                     with CicSubstitution.DeliftingWouldCaptureAFreeVariable -> 
                        None,ugraph4,metasenv,subst
                in
                match candidate with
-- 
2.39.2