incomplete irrelevance test commented out

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 886a982efb9e29735111dda4026666dbc5137157..de633357c9b1692a2964e74e824dba2b7efcc683 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1082,7 +1082,8 @@ let typecheck_subst ~metasenv subst =
     ) [] subst)
 ;;
 
-let check_rel1_irrelevant ~metasenv ~subst context =
+let check_rel1_irrelevant ~metasenv ~subst context = fun _ -> ()
+(*
   let shift e (k, context) = k+1,e::context in
   let rec aux (evil, context as k) () t =
     match R.whd ~subst context t with
@@ -1111,8 +1112,10 @@ let check_rel1_irrelevant ~metasenv ~subst context =
     | t -> U.fold shift k aux () t
   in 
     aux (1, context) ()
+*)
 
-let check_relevance ~metasenv ~subst ~in_type relevance = 
+let check_relevance ~metasenv ~subst ~in_type relevance = fun _ -> ()
+(*
   let shift e (in_type, context, relevance) = 
     assert (relevance = []); in_type, e::context, relevance
   in
@@ -1170,6 +1173,7 @@ let check_relevance ~metasenv ~subst ~in_type relevance =
        aux k () t
   in
     aux2 (in_type, [], relevance)
+*)
 ;;
 
 let typecheck_obj (uri,_height,metasenv,subst,kind) =