X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnDestructTac.ml;h=c9e46dc2af1b8523109f4b594705afb33c7435f7;hb=432d0f324b7246c91f20545867c0da4bd25f588e;hp=de4c23a1c92ae039174ff20035fb76d96a3f6e69;hpb=5a88ca4db8f9d97a58add90a8a23f06960d9364f;p=helm.git

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index de4c23a1c..c9e46dc2a 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";
@@ -468,6 +469,11 @@ let subst_tac ~context ~dir skip cur_eq =
       | NCic.Rel var ->
         cascade_select_in_ctx status ~subst:(get_subst status) context skip (var+cur_eq)
       | _ -> cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
+    let varname = match var with
+      | NCic.Rel var -> 
+          let name,_ = List.nth context var in [name]
+      | _ -> []
+    in      
     let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in
     if (List.exists (fun x -> List.mem x skip) names_to_gen)
       then oldstatus
@@ -486,7 +492,12 @@ let subst_tac ~context ~dir skip cur_eq =
                    ~what:("",0,mk_id eq_name) ~where:default_pattern;
 (*                 NTactics.reduce_tac ~reduction:(`Normalize true)
                    ~where:default_pattern;*)
+                 (* XXX: temo che la clear multipla funzioni bene soltanto se
+                  * gli identificatori sono nell'ordine giusto.
+                  * Per non saper né leggere né scrivere, usiamo due clear
+                  * invece di una *)		   
                  NTactics.try_tac (NTactics.clear_tac [eq_name]);
+		 NTactics.try_tac (NTactics.clear_tac varname);
 ]@
                  (List.map NTactics.intro_tac (List.rev names_to_gen))) status
 ;;