]> matita.cs.unibo.it Git - helm.git/commitdiff
Wrong error message patched.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 5 Mar 2004 16:20:29 +0000 (16:20 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 5 Mar 2004 16:20:29 +0000 (16:20 +0000)
helm/ocaml/cic_proof_checking/cicTypeChecker.ml

index d8d4f25f73c7cad056cce7a9003acb2277c674e5..431449e43886c6614f5e6c8b4c417e90e75fefe4 100644 (file)
@@ -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