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 6ce59e2631f26d37a6abb8535d0975539a613fdd..a1fe5d3b1be09b4c3b1d310e685ea3cf177bb44d 100644 (file)
--- 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