(Some candidate),ugraph4,metasenv,subst
| (constructor_args_no,_,instance,_)::tl ->
try
- let instance' =
- CicMetaSubst.delift_rels 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' =
- CicMetaSubst.delift_rels
- constructor_args_no
- (CicMetaSubst.apply_subst subst instance)
+ let instance',subst,metasenv =
+ CicMetaSubst.delift_rels subst metasenv
+ constructor_args_no instance
in
let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv