From 0c2737f166a10e0799c9f3d3c260c26c29c403de Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 13 Oct 2008 15:51:55 +0000 Subject: [PATCH] better error message --- helm/software/components/ng_kernel/nCicReduction.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 015ba007a..d37fdd441 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -221,7 +221,12 @@ let are_convertible ?(subst=[]) = (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)) l1 l2 - with Invalid_argument _ -> assert false) -> true + with Invalid_argument "List.for_all2" -> + prerr_endline ("Meta " ^ string_of_int n1 ^ + " occurrs with local contexts of different lenght\n"^ + NCicPp.ppterm ~metasenv:[] ~subst ~context t1 ^ " === " ^ + NCicPp.ppterm ~metasenv:[] ~subst ~context t2); + assert false) -> true | C.Meta (n1,l1), _ -> (try -- 2.39.2