- NCicUnification.unify status metasenv subst context t meta
- in
- pp (lazy ( "UNIFICATION in CTX:\n"^
- status#ppcontext ~metasenv ~subst context
- ^ "\nMENV: " ^
- status#ppmetasenv metasenv ~subst
- ^ "\nOF: " ^
- status#ppterm ~metasenv ~subst ~context newtype ^ " === " ^
- status#ppterm ~metasenv ~subst ~context expty ^ "\n"));
- let metasenv, subst =
- if perform_unification then
- NCicUnification.unify status metasenv subst context newtype expty
- else metasenv, subst
- in
- metasenv, subst, newterm, newtype
+ NCicUnification.unify status metasenv subst context t meta in
+ match expty with
+ `XTSome expty ->
+ pp (lazy ( "UNIFICATION in CTX:\n"^
+ status#ppcontext ~metasenv ~subst context
+ ^ "\nMENV: " ^
+ status#ppmetasenv metasenv ~subst
+ ^ "\nOF: " ^
+ status#ppterm ~metasenv ~subst ~context newtype ^ " === " ^
+ status#ppterm ~metasenv ~subst ~context expty ^ "\n"));
+ let metasenv,subst =
+ NCicUnification.unify status metasenv subst context newtype expty
+ in
+ metasenv, subst, newterm, newtype
+ | `XTSort ->
+ (match NCicReduction.whd status ~subst context newtype with
+ C.Sort _ -> metasenv,subst,newterm,newtype
+ | _ -> first exc tl)
+ | `XTInd ->
+ (match NCicReduction.whd status ~subst context newtype with
+ C.Const (Ref.Ref (_, Ref.Ind _)) -> metasenv,subst,newterm,newtype
+ | _ -> first exc tl)
+ | `XTProd ->
+ (match NCicReduction.whd status ~subst context newtype with
+ C.Prod _ -> metasenv,subst,newterm,newtype
+ | _ -> first exc tl)