Failure ==> DeliftingWouldCaptureAFreeVariable
exception ReferenceToConstant;;
exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
exception ReferenceToConstant;;
exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
+exception DeliftingWouldCaptureAFreeVariable;;
let debug_print = fun _ -> ()
let debug_print = fun _ -> ()
if m < k then
C.Rel m
else if m < k + n then
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) ->
else
C.Rel (m - n)
| C.Var (uri,exp_named_subst) ->
exception ReferenceToVariable;;
exception ReferenceToConstant;;
exception ReferenceToInductiveDefinition;;
exception ReferenceToVariable;;
exception ReferenceToConstant;;
exception ReferenceToInductiveDefinition;;
+exception DeliftingWouldCaptureAFreeVariable;;
(* lift n t *)
(* lifts [t] of [n] *)
(* lift n t *)
(* lifts [t] of [n] *)
in
candidate_oty,ugraph,metasenv,subst
with
in
candidate_oty,ugraph,metasenv,subst
with
+ CicSubstitution.DeliftingWouldCaptureAFreeVariable
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
None,ugraph,metasenv,subst
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
None,ugraph,metasenv,subst
Some
(add_lambdas 0 t arity_instantiated_with_left_args),
ugraph,metasenv,subst
Some
(add_lambdas 0 t arity_instantiated_with_left_args),
ugraph,metasenv,subst
+ with CicSubstitution.DeliftingWouldCaptureAFreeVariable ->
None,ugraph4,metasenv,subst
in
match candidate with
None,ugraph4,metasenv,subst
in
match candidate with