X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=4b00edd05b2878ccea79ea6712540c2cfaf7db2a;hb=44ccb088991b937c54cbe13f0a135e36da9d5d8d;hp=76bedd833bebcbe97d70c6ba9a28a118e9bff3c6;hpb=5fa934e50e1cfd80175ab2a6674dc9bc4bd2281b;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 76bedd833..4b00edd05 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1015,8 +1015,10 @@ and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te =
  | C.Rel m when List.mem m safes -> true
  | C.Lambda (name, s, t) ->
      is_really_smaller ~subst ~metasenv (shift_k (name, C.Decl s) k) t
- | C.Rel _ 
+ | C.Appl (he::_) ->
+     is_really_smaller ~subst ~metasenv k he
  | C.Appl _
+ | C.Rel _ 
  | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
  | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false
    (*| C.Fix (_, fl) ->