let _,_,t,_ = NCicUtils.lookup_subst i subst in
let t = NCicSubstitution.subst_meta lc t in
eat_lambdas ctx t
- with Not_found -> ctx, t)
+ with NCicUtils.Subst_not_found _ -> ctx, t)
| t -> ctx, t
in
let context_body = eat_lambdas [] t in
if is_type attrs then
metasenv,subst,true
else
+ let _,cc,ty = NCicUtils.lookup_meta n metasenv in
+ let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
let metasenv =
NCicUntrusted.replace_in_metasenv n
- (fun attrs,cc,ty -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
+ (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
metasenv
in
metasenv,subst,false
if is_type attrs then
metasenv,subst,true
else
+ let _,cc,_,ty = NCicUtils.lookup_subst n subst in
+ let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
let subst =
NCicUntrusted.replace_in_subst n
- (fun attrs,cc,bo,ty->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
+ (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
subst
in
optimize_meta metasenv subst (NCicSubstitution.subst_meta lc bo))
| _ -> assert false)
| `IsType
| `IsTerm ->
- (match ty,t with
- NCic.Implicit (`Typeof _), _ ->
+ (match ty with
+ NCic.Implicit (`Typeof _) ->
let (metasenv, subst), ty_t =
try
NCicMetaSubst.delift
in
delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
subst
- | _, _ ->
+ | _ ->
let lty = NCicSubstitution.subst_meta lc ty in
pp (lazy ("On the types: " ^
ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
| NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
+ | C.Meta (n,_), C.Meta (m,lc') when
+ let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
+ let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
+ (n < m && cc1 = cc2) ||
+ let len1 = List.length cc1 in
+ let len2 = List.length cc2 in
+ len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
+ instantiate rdb test_eq_only metasenv subst context m lc'
+ (NCicReduction.head_beta_reduce ~subst t1) (not swap)
| C.Meta (n,lc), t ->
instantiate rdb test_eq_only metasenv subst context n lc
(NCicReduction.head_beta_reduce ~subst t) swap
(NCicTypeChecker.typeof ~metasenv ~subst context meta)
in
let metasenv, subst =
- try
- unify rdb test_eq_only metasenv subst context
- (C.Meta (i,l)) lambda_Mj swap
- with UnificationFailure msg | Uncertain msg when not norm2->
- (* failure: let's try again argument vs argument *)
- raise (KeepReducing msg)
+ unify rdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj swap
in
let metasenv, subst =
unify rdb test_eq_only metasenv subst context t1 t2 swap
with
Invalid_argument _ ->
raise (Uncertain (mk_msg metasenv subst context t1 t2))
- | UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
- raise (KeepReducing (mk_msg metasenv subst context t1 t2))
| KeepReducing _ | KeepReducingThis _ -> assert false
in
metasenv, subst
| (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
- C.Match (ref2,outtype2,term2,pl2)) ->
+ C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
let _,_,ty,_ = List.nth itl tyno in
let rec remove_prods ~subst context ty =
| C.Sort C.Prop -> true
| _ -> false
in
- if not (Ref.eq ref1 ref2) then
+ (* if not (Ref.eq ref1 ref2) then
raise (Uncertain (mk_msg metasenv subst context t1 t2))
- else
+ else*)
let metasenv, subst =
unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
let metasenv, subst =
| _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2))
(*D*) in outside None; rc with exn -> outside (Some exn); raise exn
in
+ let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
+ try fo_unif test_eq_only metasenv subst nt1 nt2
+ with
+ UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
+ raise (KeepReducing (mk_msg metasenv subst context t1 t2))
+ in
let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
(*D*) inside 'H'; try let rc =
pp(lazy ("\nProblema:\n" ^