Wrong error message patched.

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index d8d4f25f73c7cad056cce7a9003acb2277c674e5..431449e43886c6614f5e6c8b4c417e90e75fefe4 100644 (file)
--- 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