From f2f9699ce6c656e62ae18148bce61f8bb945dc7a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 14 May 2008 16:49:25 +0000 Subject: [PATCH] Bug fixed: types were check for conversion in the wrong context. --- .../software/components/ng_kernel/nCicTypeChecker.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index fc6d04a03..2f8f69a41 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -985,14 +985,14 @@ let typecheck_context ~metasenv ~subst context = | name,C.Def (te,ty) -> ignore (typeof ~metasenv ~subst:[] context ty); let ty' = typeof ~metasenv ~subst:[] context te in - if not (R.are_convertible ~subst [] ty' ty) then + if not (R.are_convertible ~subst context ty' ty) then raise (AssertFailure (lazy (Printf.sprintf ( "the type of the definiens for %s in the context is not "^^ "convertible with the declared one.\n"^^ "inferred type:\n%s\nexpected type:\n%s") name - (PP.ppterm ~subst ~metasenv ~context:[] ty') - (PP.ppterm ~subst ~metasenv ~context:[] ty)))) + (PP.ppterm ~subst ~metasenv ~context ty') + (PP.ppterm ~subst ~metasenv ~context ty)))) end; d::context ) context []) @@ -1024,14 +1024,14 @@ let typecheck_subst ~metasenv subst = typecheck_context ~metasenv ~subst context; ignore (typeof ~metasenv ~subst context ty); let ty' = typeof ~metasenv ~subst context bo in - if not (R.are_convertible ~subst [] ty' ty) then + if not (R.are_convertible ~subst context ty' ty) then raise (AssertFailure (lazy (Printf.sprintf ( "the type of the definiens for %d in the substitution is not "^^ "convertible with the declared one.\n"^^ "inferred type:\n%s\nexpected type:\n%s") i - (PP.ppterm ~subst ~metasenv ~context:[] ty') - (PP.ppterm ~subst ~metasenv ~context:[] ty)))); + (PP.ppterm ~subst ~metasenv ~context ty') + (PP.ppterm ~subst ~metasenv ~context ty)))); subst @ [conj] ) [] subst) ;; -- 2.39.2