Better error message.

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 3459c8dd246b34e48848b367491465d324bd0b7c..61cda8a336235e70c66cc14ed72f17e78a1679c6 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1089,7 +1089,10 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) =
   | (_,h1,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,Ref.Def h2) ->
      if h1 <> h2 then error ();
      ty
-  | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
+  | _ ->
+    raise (AssertFailure
+     (lazy ("type_of_constant: environment/reference: " ^
+       Ref.string_of_reference ref)))
 
 and get_relevance ~metasenv ~subst context t args = 
    let ty = typeof ~subst ~metasenv context t in