From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 4 Jun 2008 15:22:50 +0000 (+0000)
Subject: incomplete irrelevance test commented out
X-Git-Tag: make_still_working~5086
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dace8da2fbdb8208953d3392ff187f7e8616b83f;p=helm.git

incomplete irrelevance test commented out
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 886a982ef..de633357c 100644
--- 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) =