From 24dd4569daf1d35bffaa813b8164058d8643f14d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 16 Nov 2007 09:04:05 +0000
Subject: [PATCH] added default for matita.noiinertypes

---
 matita/matitaInit.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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 *)
 ]
-- 
2.39.2