From 32f9135944b5d2979f12d2a66135702c7d230341 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 20 Oct 2011 12:49:31 +0000 Subject: [PATCH] Removed some unneeded normalizations from the generation of discrimination principles (they had a bad effect on performance). --- matita/components/ng_tactics/nDestructTac.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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"; -- 2.39.2