From fdc7fbf786e14766cc598c75fae0650c219d679a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Mar 2006 14:53:13 +0000 Subject: [PATCH] Debugging code removed. --- components/grafite_engine/grafiteEngine.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 0bbb01403..bfd0aff59 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -418,7 +418,6 @@ let refinement_toolkit = { let eval_coercion status ~add_composites uri = let basedir = Helm_registry.get "matita.basedir" in let status,compounds = - prerr_endline "evaluating a coercion command"; GrafiteSync.add_coercion ~basedir ~add_composites refinement_toolkit status uri in let moo_content = coercion_moo_statement_of uri in let status = GrafiteTypes.add_moo_content [moo_content] status in -- 2.39.2