From d50309307c1dc85341759a020d7052b4a1d025b3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 18 Apr 2008 13:59:17 +0000 Subject: [PATCH] Appl case in is_really_smaller fixed as in the old kernel --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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) -> -- 2.39.2