some cosmetic fixes

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 0496076e73b26a9968d1eb59b7f9f3e15c4c6029..10fe24030d00c27951d49580f499fbd5c2c49754 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -1,8 +1,9 @@
 
 open Printf
-
 open MatitaTypes
 
+let debug = true ;;
+let debug_print = if debug then prerr_endline else ignore ;;
 
 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   * names as long as they are available, then it fallbacks to name generation
@@ -253,7 +254,7 @@ let eval_command status cmd =
       in
       {status with proof_status = No_proof}
   | TacticAst.Theorem (_, _, None, _, _) ->
-      command_error "The grammas should avoid having unnamed theorems!"
+      command_error "The grammar should avoid having unnamed theorems!"
   | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
   | TacticAst.Alias (loc, spec) -> 
       match spec with