From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 20 Oct 2011 12:49:31 +0000 (+0000)
Subject: Removed some unneeded normalizations from the generation of discrimination
X-Git-Tag: make_still_working~2169
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=32f9135944b5d2979f12d2a66135702c7d230341;p=helm.git

Removed some unneeded normalizations from the generation of discrimination
principles (they had a bad effect on performance).
---

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index de4c23a1c..12a1efd7e 100644
--- a/matita/components/ng_tactics/nDestructTac.ml
+++ b/matita/components/ng_tactics/nDestructTac.ml
@@ -340,7 +340,8 @@ let mk_discriminator ~use_jmeq name it leftno status baseuri =
     let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
     (* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *)
     let params = List.map (fun x -> NTactics.intro_tac ("a" ^ string_of_int x)) nlist in
-        NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern::
+        (* NTactics.reduce_tac ~reduction:(`Normalize true)
+         * ~where:default_pattern::*)
         params @ [
         NTactics.intro_tac "P";
         NTactics.intro_tac "DH";
@@ -364,8 +365,8 @@ let mk_discriminator ~use_jmeq name it leftno status baseuri =
 
   let status =
    NTactics.block_tac (
-    [print_tac (lazy "ci sono");
-     NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern 
+    [print_tac (lazy "ci sono") (*;
+     NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern *)
     ]
   @ List.map (fun x -> NTactics.intro_tac x) params @
     [NTactics.intro_tac "x";