(Some candidate),ugraph4,metasenv,subst
| (constructor_args_no,_,instance,_)::tl ->
try
- let instance' =
- CicSubstitution.delift constructor_args_no
- (CicMetaSubst.apply_subst subst instance)
+ let instance',subst,metasenv =
+ CicMetaSubst.delift_rels subst metasenv
+ constructor_args_no instance
in
let candidate,ugraph,metasenv,subst =
List.fold_left (
| None -> None,ugraph,metasenv,subst
| Some ty ->
try
- let instance' =
- CicSubstitution.delift
- constructor_args_no
- (CicMetaSubst.apply_subst subst instance)
+ let instance',subst,metasenv =
+ CicMetaSubst.delift_rels subst metasenv
+ constructor_args_no instance
in
-prerr_endline ("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
-prerr_endline ("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