let (===) x y = Pervasives.compare x y = 0 ;;
-let get_relevance = ref (fun _ ~metasenv:_ ~subst:_ _ _ -> assert false);;
+let get_relevance = ref (fun (_:#NCicEnvironment.status) ~metasenv:_ ~subst:_ _ _ -> assert false);;
let set_get_relevance = (:=) get_relevance;;
-let alpha_eq (status:#NCic.status) ~test_lambda_source aux test_eq_only metasenv subst context
+let alpha_eq (status:#NCicEnvironment.status) ~test_lambda_source aux test_eq_only metasenv subst context
t1 t2 =
if t1 === t2 then
true
else
match (t1,t2) with
| C.Sort s1, C.Sort s2 ->
- NCicEnvironment.are_sorts_convertible ~test_eq_only s1 s2
+ NCicEnvironment.are_sorts_convertible status ~test_eq_only s1 s2
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
aux true context s1 s2 &&
with Invalid_argument _ -> false
| HExtlib.FailureAt fail ->
let relevance =
- !get_relevance (status :> NCic.status) ~metasenv ~subst context hd1 tl1 in
+ !get_relevance (status :> NCicEnvironment.status) ~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 (status :> NCic.status) ~metasenv ~subst context hd1 tl1 in
+ let relevance = !get_relevance (status :> NCicEnvironment.status) ~metasenv ~subst context hd1 tl1 in
(try
HExtlib.list_forall_default3
(fun t1 t2 b -> not b || aux true context t1 t2)