]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaEngine.ml
added query
[helm.git] / helm / matita / matitaEngine.ml
index bb2e3c1a66cfc675fe2dc015a93119429fc0f295..354ecd9e819424cccf20424c31f99604a0252212 100644 (file)
@@ -523,7 +523,7 @@ let eval_command status cmd =
      match obj with
         Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
          let name = UriManager.name_of_uri uri in
-        if not(CicPp.check name ty) then
+         if not(CicPp.check name ty) then
            MatitaLog.warn ("Bad name: " ^ name);
          assert (metasenv = metasenv');
          let goalno =