From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 16 Nov 2007 09:04:05 +0000 (+0000)
Subject: added default for matita.noiinertypes
X-Git-Tag: 0.4.96@7881~4
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=24dd4569daf1d35bffaa813b8164058d8643f14d;p=helm.git

added default for matita.noiinertypes
---

diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml
index c25113f26..3beb85ca6 100644
--- a/matita/matitaInit.ml
+++ b/matita/matitaInit.ml
@@ -50,7 +50,8 @@ let registry_defaults = [
   "matita.system",               "false";
   "matita.verbosity",            "1";
   "matita.bench",                "false";
-  "matita.paste_unicode_as_tex", "false"
+  "matita.paste_unicode_as_tex", "false";
+  "matita.noinnertypes",         "false";
     (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
      * intuitively verbose *)
 ]