From 676523786dfa270a37f4566c5d265034a67311da Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 Nov 2007 09:04:05 +0000 Subject: [PATCH] added default for matita.noiinertypes --- helm/software/matita/matitaInit.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 *) ] -- 2.39.2