From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 16 May 2008 11:52:59 +0000 (+0000)
Subject: used ind/coind information in references
X-Git-Tag: make_still_working~5191
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18c6034717c91fda434f47a0aa3b16001e1dd352;p=helm.git

used ind/coind information in references
---

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