- changed command line interface of cicbrowser so that everything which could be...

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 89481b287434a12284dedd67c24e76c08acee8e5..8c891b04355759f28ff7a8522329fed6dcb54293 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -711,7 +711,7 @@ let eval_command opts status cmd =
          if metasenv <> [] then
           command_error (
             "metasenv not empty while giving a definition with body: " ^
-            CicMetaSubst.ppmetasenv metasenv []);
+            CicMetaSubst.ppmetasenv [] metasenv);
          let status = MatitaSync.add_obj uri obj status in
           match obj with
              Cic.Constant _ -> status