| (C.Sort _ ,_)
| (_, C.Sort _)
| (C.Implicit, _)
- | (_, C.Implicit) -> if R.are_convertible t1 t2 then subst
+ | (_, C.Implicit) -> if R.are_convertible context t1 t2 then subst
else raise UnificationFailed
| (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2
| (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te
| (C.MutInd _, _)
| (_, C.MutInd _)
| (C.MutConstruct _, _)
- | (_, C.MutConstruct _) -> if R.are_convertible t1 t2 then subst
+ | (_, C.MutConstruct _) -> if R.are_convertible context t1 t2 then subst
else raise UnificationFailed
| (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
let subst' = fo_unif_aux subst k outt1 outt2 in
| (C.Fix _, _)
| (_, C.Fix _)
| (C.CoFix _, _)
- | (_, C.CoFix _) -> if R.are_convertible t1 t2 then subst
+ | (_, C.CoFix _) -> if R.are_convertible context t1 t2 then subst
else raise UnificationFailed
| (_,_) -> raise UnificationFailed
in fo_unif_aux [] 0 t1 t2;;
try
let t = List.assoc i subst in
let t' = um_aux 0 t in
- unwinded := (i,t)::!unwinded ;
+ unwinded := (i,t')::!unwinded ;
S.lift k t'
with
Not_found ->
- (* not constrained variable, i.e. free in subst *)
+ (* not constrained variable, i.e. free in subst*)
C.Meta i
in
frozen := saved_frozen ;
;;
(* UNWIND THE MGU INSIDE THE MGU *)
-(* let unwind mgu =
- let mark = Array.make (Array.length mgu) 0 in
- Array.iter (fun x -> let foo = unwind_meta mgu mark x in ()) mgu; mgu;; *)
-
let unwind_subst subst =
List.fold_left
(fun unwinded (i,_) -> snd (unwind subst unwinded (Cic.Meta i))) [] subst