]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicTypeChecker.ml
- pretty printer made robust in face of list_nth
[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml
index f459c602432ae5888539bca809925da3ae49f775..65f17ee38ef4c356e4e5a5d1f6c3a3d16d36778c 100644 (file)
@@ -350,7 +350,9 @@ let type_of_branch ~subst context leftno outty cons tycons =
         | t -> C.Appl [t ; C.Rel 1]
        in
         C.Prod (name,so, aux (liftno+1) ((name,(C.Decl so))::context) cons de)
-   | _ -> raise (AssertFailure (lazy "type_of_branch"))
+   | t -> raise (AssertFailure 
+      (lazy ("type_of_branch, the contructor has type: " ^ NCicPp.ppterm
+       ~metasenv:[] ~context:[] ~subst:[] t)))
  in
   aux 0 context cons tycons
 ;;