X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=431449e43886c6614f5e6c8b4c417e90e75fefe4;hb=72e89daa67c3a5925e68c86d0109eceaffd1f163;hp=d8d4f25f73c7cad056cce7a9003acb2277c674e5;hpb=3fec2330f2d30d47ebca0decd30bd2a457a9cbd3;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index d8d4f25f7..431449e43 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1623,7 +1623,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
          | Cic.Variable (_,None,_,_) -> ()
          | _ ->
             raise (TypeCheckerFailure
-              ("Unknown mutual inductive definition:" ^
+              ("Unknown variable definition:" ^
               UriManager.string_of_uri uri))
        ) ;
        let typeoft = type_of_aux context t in