Exception raised by delift changed:

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

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
index b1c09277ba989b086d06e07ab091811f19d1c5b1..5c8fa7ca59b8e31bc3019f71ef0a3cbd91ac0354 100644 (file)
--- 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] *)