From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 May 2008 16:49:25 +0000 (+0000)
Subject: Bug fixed: types were check for conversion in the wrong context.
X-Git-Tag: make_still_working~5207
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f2f9699ce6c656e62ae18148bce61f8bb945dc7a;p=helm.git

Bug fixed: types were check for conversion in the wrong context.
---

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)
 ;;