Swapped arguments in error message.

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 3d0f13e2b582440fcc99af9ef83b78411d06acb0..dfb014c20d8ada6c609823153632d701b299cee2 100644 (file)
--- 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"))