From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 8 Apr 2008 21:49:50 +0000 (+0000)
Subject: Swapped arguments in error message.
X-Git-Tag: make_still_working~5389
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c25986cdbd05f0c06d93f850453b5f82695b7814;p=helm.git

Swapped arguments in error message.
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 3d0f13e2b..dfb014c20 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -561,8 +561,8 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty =
                    "\n%s\nbut is should have type \n%s\n")
                   (NCicPp.ppterm ~subst ~metasenv ~context he)
                   (NCicPp.ppterm ~subst ~metasenv ~context arg)
-                  (NCicPp.ppterm ~subst ~metasenv ~context s)
-                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg))))
+                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg)
+                  (NCicPp.ppterm ~subst ~metasenv ~context s))))
        | _ ->
           raise 
             (TypeCheckerFailure
@@ -681,11 +681,11 @@ let rec typeof ~subst ~metasenv context term =
        let ty_he = typeof_aux context he in
        let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
 (*
-       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~context ty_he);
+       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he);
        prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map snd args_with_ty)));
+       ~subst ~metasenv ~context) (List.map snd args_with_ty)));
        prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map fst args_with_ty)));
+       ~subst ~metasenv ~context) (List.map fst args_with_ty)));
 *)
        eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))