X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.mli;h=5c8fa7ca59b8e31bc3019f71ef0a3cbd91ac0354;hb=47c9a0967ce271e551d4cbc8ac388097d774a3ef;hp=b1c09277ba989b086d06e07ab091811f19d1c5b1;hpb=4c1967e287c35d226e773df8d221293c3c74c9d4;p=helm.git 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] *)