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
(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" ^