Appl case in is_really_smaller fixed as in the old kernel

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 76bedd833bebcbe97d70c6ba9a28a118e9bff3c6..4b00edd05b2878ccea79ea6712540c2cfaf7db2a 100644 (file)
--- 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) ->