From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 17 Apr 2008 16:55:36 +0000 (+0000)
Subject: example:
X-Git-Tag: make_still_working~5326
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=6ebe894ff0fee5d99bad615ce053128292657dee;p=helm.git

example:
  inductive I : Type :=
  | k : \forall A. (A -> I)-> I

  match t with
  | k _ f => f w (* is smaller than t even if applied! *)
---

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 883bc3296..9336cb84a 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -763,10 +763,12 @@ and check_is_really_smaller_arg
  match CicReduction.whd ~subst context te with
      C.Rel m when List.mem m safes -> true
    | C.Rel _ 
-   | C.Appl _
    | C.MutConstruct _
    | C.Const _
    | C.Var _ -> false
+   | C.Appl (he::_) ->
+        check_is_really_smaller_arg rec_uri rec_uri_len 
+          ~logger ~metasenv ~subst context n nn kl x safes he
    | C.Lambda (name,ty,ta) ->
       check_is_really_smaller_arg rec_uri rec_uri_len 
         ~logger ~metasenv ~subst (Some (name,Cic.Decl ty)::context)