let (===) x y = Pervasives.compare x y = 0 ;;
-let get_relevance = ref (fun ~subst:_ _ _ -> assert false);;
+let get_relevance = ref (fun ~metasenv:_ ~subst:_ _ _ -> assert false);;
let set_get_relevance f = get_relevance := f;;
(* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[]) =
+let are_convertible ~metasenv ~subst =
let rec aux test_eq_only context t1 t2 =
let alpha_eq test_eq_only t1 t2 =
if t1 === t2 then
with Invalid_argument "List.for_all2" ->
prerr_endline ("Meta " ^ string_of_int n1 ^
" occurrs with local contexts of different lenght\n"^
- NCicPp.ppterm ~metasenv:[] ~subst ~context t1 ^ " === " ^
- NCicPp.ppterm ~metasenv:[] ~subst ~context t2);
+ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t2);
assert false) -> true
| C.Meta (n1,l1), _ ->
tl1 tl2 true relevance
with Invalid_argument _ -> false
| HExtlib.FailureAt fail ->
- let relevance = !get_relevance ~subst context hd1 tl1 in
+ let relevance =
+ !get_relevance ~metasenv ~subst context hd1 tl1 in
let _,relevance = HExtlib.split_nth fail relevance in
let b,relevance = (match relevance with
| [] -> assert false
| (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
aux test_eq_only context hd1 hd2 &&
- let relevance = !get_relevance ~subst context hd1 tl1 in
+ let relevance = !get_relevance ~metasenv ~subst context hd1 tl1 in
(try
HExtlib.list_forall_default3
(fun t1 t2 b -> not b || aux test_eq_only context t1 t2)