(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
-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
candidate outtype ugraph5
in
C.MutCase (uri, i, outtype, term', pl'),
- (Cic.Appl (outtype::right_args@[term'])),
+ CicReduction.head_beta_reduce
+ (CicMetaSubst.apply_subst subst
+ (Cic.Appl (outtype::right_args@[term']))),
subst,metasenv,ugraph)
| _ -> (* easy case *)
let _,_, subst, metasenv,ugraph5 =
(subst,metasenv,ugraph5) outtypeinstances
in
C.MutCase (uri, i, outtype, term', pl'),
- CicReduction.whd ~subst context
- (C.Appl(outtype::right_args@[term])),
+ CicReduction.head_beta_reduce
+ (CicMetaSubst.apply_subst subst
+ (C.Appl(outtype::right_args@[term]))),
subst,metasenv,ugraph6)
| C.Fix (i,fl) ->
let fl_ty',subst,metasenv,types,ugraph1 =