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 fc6d04a038dfa2c91ee102100d82d83bf7151d93..2f8f69a41b8b77b1e629b0ea683a395bddba74cc 100644 (file)
--- 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)
 ;;