From dace8da2fbdb8208953d3392ff187f7e8616b83f Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 4 Jun 2008 15:22:50 +0000 Subject: [PATCH] incomplete irrelevance test commented out --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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) = -- 2.39.2