This commit patches the environment and the library so that their status is

[helm.git] / matitaB / components / ng_kernel / nCicReduction.ml

diff --git a/matitaB/components/ng_kernel/nCicReduction.ml b/matitaB/components/ng_kernel/nCicReduction.ml
index 8a84810a3cfd456d39b4199ae48f46d054f0793a..4fd42aa280dca4d300cf248452900eca74fe3481 100644 (file)
--- a/matitaB/components/ng_kernel/nCicReduction.ml
+++ b/matitaB/components/ng_kernel/nCicReduction.ml
@@ -208,18 +208,18 @@ let whd = R.whd
 
 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 &&
@@ -285,7 +285,7 @@ let alpha_eq (status:#NCic.status) ~test_lambda_source aux test_eq_only metasenv
         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
@@ -302,7 +302,7 @@ let alpha_eq (status:#NCic.status) ~test_lambda_source aux test_eq_only metasenv
 
    | (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)