| (constructor_args_no,_,instance,_)::tl ->
try
let instance' =
- CicSubstitution.delift constructor_args_no
+ CicMetaSubst.delift_rels constructor_args_no
(CicMetaSubst.apply_subst subst instance)
in
let candidate,ugraph,metasenv,subst =
| Some ty ->
try
let instance' =
- CicSubstitution.delift
+ CicMetaSubst.delift_rels
constructor_args_no
(CicMetaSubst.apply_subst subst instance)
in
-debug_print ("PRIMA subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst);
let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv
instance' ty ugraph
in
-debug_print ("DOPO subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst);
candidate_oty,ugraph,metasenv,subst
-(* CSC: XXX
- let b,ugraph1 =
- CicReduction.are_convertible context
- instance' ty ugraph
- in
- if b then
- candidate_oty,ugraph1,metasenv
- else
- None,ugraph,metasenv
-*)
with
- Failure _
+ CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
None,ugraph,metasenv,subst
Some
(add_lambdas 0 t arity_instantiated_with_left_args),
ugraph,metasenv,subst
- with Failure s ->
+ with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
None,ugraph4,metasenv,subst
in
match candidate with