From 26b754bcd3763fd7624637adab0635edefa1168f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Apr 2008 11:55:43 +0000 Subject: [PATCH] lefts_and_tys was tys@lefts, CSC claims it was working since that context is only used by whd and it did not contain any definitions by contructions, thus the length was the only important bit --- .../components/cic_proof_checking/cicTypeChecker.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index dd25edac4..eb9d376f2 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -801,7 +801,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = | (_,_,ty,_)::_ -> fst (split_prods ~subst [] paramsno ty) in - (tys@lefts,List.length tl,isinductive,paramsno,cl') + (lefts@tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -852,7 +852,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = | (_,_,ty,_)::_ -> fst (split_prods ~subst [] paramsno ty) in - (tys@lefts,List.length tl,isinductive,paramsno,cl') + (lefts@tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -1006,7 +1006,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = | (_,_,ty,_)::_ -> fst (split_prods ~subst [] paramsno ty) in - (tys@lefts,len,isinductive,paramsno,cl') + (lefts@tys,len,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -1059,7 +1059,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = | (_,_,ty,_)::_ -> fst (split_prods ~subst [] paramsno ty) in - (tys@lefts,List.length tl,isinductive,paramsno,cl') + (lefts@tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ -- 2.39.2