From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Mar 2004 16:20:29 +0000 (+0000)
Subject: Wrong error message patched.
X-Git-Tag: v0_0_4~42
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=72e89daa67c3a5925e68c86d0109eceaffd1f163;p=helm.git

Wrong error message patched.
---

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