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: make_still_working~5825
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=676523786dfa270a37f4566c5d265034a67311da;hp=af7ecc71c93a6c30f822e9d23175be7bb24f3f63;p=helm.git

added default for matita.noiinertypes
---

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index c25113f26..3beb85ca6 100644
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/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 *)
 ]