better error message

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 015ba007a311a8fb6491c84c58034215d92b6173..d37fdd441d3c689772e28fd9dd7e20712b6ac2d1 100644 (file)
--- 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