From 6ebe894ff0fee5d99bad615ce053128292657dee Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 17 Apr 2008 16:55:36 +0000 Subject: [PATCH] example: inductive I : Type := | k : \forall A. (A -> I)-> I match t with | k _ f => f w (* is smaller than t even if applied! *) --- helm/software/components/cic_proof_checking/cicTypeChecker.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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) -- 2.39.2