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

[helm.git] / matitaB / components / ng_refiner / nCicUnification.ml

diff --git a/matitaB/components/ng_refiner/nCicUnification.ml b/matitaB/components/ng_refiner/nCicUnification.ml
index 1e37ff79793ba03894f306c0be69acb50bbe7115..cd5c89dd33a785d4830a1ef51d79637f91e2c369 100644 (file)
--- a/matitaB/components/ng_refiner/nCicUnification.ml
+++ b/matitaB/components/ng_refiner/nCicUnification.ml
@@ -164,7 +164,7 @@ let rec lambda_intros status metasenv subst context argsno ty =
   
 let unopt exc = function None -> raise exc | Some x -> x ;;
 
-let fix (status:#NCic.status) metasenv subst is_sup test_eq_only exc t =
+let fix (status:#NCicEnvironment.status) metasenv subst is_sup test_eq_only exc t =
   (*D*)  inside 'f'; try let rc =  
   pp (lazy (status#ppterm ~metasenv ~subst ~context:[] t));
   let rec aux test_eq_only metasenv = function
@@ -176,10 +176,10 @@ let fix (status:#NCic.status) metasenv subst is_sup test_eq_only exc t =
        metasenv,orig
     | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc
     | NCic.Sort (NCic.Type u) when is_sup ->
-       metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u)))
+       metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup status u)))
     | NCic.Sort (NCic.Type u) ->
        metasenv, NCic.Sort (NCic.Type 
-         (unopt exc (NCicEnvironment.inf ~strict:false u)))
+         (unopt exc (NCicEnvironment.inf status ~strict:false u)))
     | NCic.Meta (n,_) as orig ->
         (try 
           let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig
@@ -335,10 +335,10 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap =
            match s,swap with
               NCic.Type u2, false ->
                NCic.Sort (NCic.Type
-                (unopt exc (NCicEnvironment.inf ~strict:false
-                 (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2))))
+                (unopt exc (NCicEnvironment.inf status ~strict:false
+                 (unopt exc (NCicEnvironment.inf status ~strict:true u1) @ u2))))
             | NCic.Type u2, true ->
-               if NCicEnvironment.universe_lt u2 u1 then
+               if NCicEnvironment.universe_lt status u2 u1 then
                 NCic.Sort (NCic.Type u2)
                else (raise exc)
             | NCic.Prop,_ -> NCic.Sort NCic.Prop
@@ -425,7 +425,7 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
            assert false 
        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
            let a, b = if swap then b,a else a,b in
-           if NCicEnvironment.universe_leq a b then metasenv, subst
+           if NCicEnvironment.universe_leq status a b then metasenv, subst
            else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
        | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
            if NCicEnvironment.universe_eq a b then metasenv, subst
@@ -566,7 +566,7 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
           let tym = NCicSubstitution.subst_meta status lc tym in
            match tyn,tym with
               NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
-               NCicEnvironment.universe_lt u1 u2
+               NCicEnvironment.universe_lt status u1 u2
             | _,_ -> false ->
           instantiate status test_eq_only metasenv subst context m lc'
             (NCicReduction.head_beta_reduce status ~subst t1) (not swap)