with
| MultiPassDisambiguator.DisambiguationError _
| NCicRefiner.RefineFailure _
+ | NCicRefiner.Uncertain _
| NCicUnification.UnificationFailure _
+ | NCicUnification.Uncertain _
| NCicTypeChecker.TypeCheckerFailure _
- | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy fname)
+ | NCicMetaSubst.MetaSubstFailure _
+ | NCicMetaSubst.Uncertain _ as exn -> fail ~exn (lazy fname)
;;
class type g_eq_status =
let u, d, metasenv, subst, o = status#obj in
pp(lazy("delifting as " ^
status#ppterm ~metasenv ~subst ~context:source
- (NCic.Meta (0,lc))));
+ (NCic.Meta (-1,lc))));
let (metasenv, subst), t =
NCicMetaSubst.delift status
~unify:(fun m s c t1 t2 ->
with
| NCicUnification.UnificationFailure _
| NCicUnification.Uncertain _ -> None)
- metasenv subst source 0 lc t
+ metasenv subst source (-1) lc t
in
let status = status#set_obj (u, d, metasenv, subst, o) in
status, (ctx,t))
let ctx = (n, NCic.Decl s2) :: ctx in
let status, t = select status ctx t1 t2 in
status, NCic.Prod (n,s,t)
- | NCic.Appl l1, NCic.Appl l2 ->
+ | NCic.Appl l1, NCic.Appl l2 when List.length l1 = List.length l2 ->
let status, l =
List.fold_left2
(fun (status,l) x y ->
(status,[]) l1 l2
in
status, NCic.Appl (List.rev l)
- | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2) ->
+ | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2)
+ when List.length pl1 = List.length pl2 ->
let status, t = select status ctx t1 t2 in
let status, ot = select status ctx ot1 ot2 in
let status, pl =