...

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

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 432ea9a45bd4c79e599181da2db0cd9038a06463..a88a1aaf388ce9f1dfd69261709ba08d5a6a1c0c 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -213,12 +213,8 @@ let alpha_eq ~test_lambda_source aux test_eq_only metasenv subst context t1 t2 =
    true
  else
    match (t1,t2) with
-   | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> 
-       NCicEnvironment.universe_leq a b
-   | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
-       NCicEnvironment.universe_eq a b
-   | (C.Sort C.Prop,C.Sort (C.Type _)) -> (not test_eq_only)
-   | (C.Sort C.Prop, C.Sort C.Prop) -> true
+   | C.Sort s1, C.Sort s2 -> 
+       NCicEnvironment.are_sorts_convertible ~test_eq_only s1 s2 
 
    | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
        aux true context s1 s2 &&