From c25986cdbd05f0c06d93f850453b5f82695b7814 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 21:49:50 +0000 Subject: [PATCH] Swapped arguments in error message. --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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")) -- 2.39.2