From 18c6034717c91fda434f47a0aa3b16001e1dd352 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 May 2008 11:52:59 +0000 Subject: [PATCH] used ind/coind information in references --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 6ce59e263..a1fe5d3b1 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -927,11 +927,9 @@ and is_really_smaller | C.Appl [] | C.Const (Ref.Ref (_,Ref.Fix _)) -> assert false | C.Meta _ -> true - | C.Match (Ref.Ref (uri,_) as ref,outtype,term,pl) -> + | C.Match (Ref.Ref (uri,Ref.Ind (isinductive,_)),outtype,term,pl) -> (match term with | C.Rel m | C.Appl (C.Rel m :: _ ) when is_safe m recfuns || m = x -> - (* TODO: add CoInd to references so that this call is useless *) - let isinductive, _, _, _, _ = E.get_checked_indtys ref in if not isinductive then List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl else -- 2.39.2