From 72e89daa67c3a5925e68c86d0109eceaffd1f163 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Mar 2004 16:20:29 +0000 Subject: [PATCH] Wrong error message patched. --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2