X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnDestructTac.ml;h=f03baa65645b5bf1e9ee33414fc0b47f89040319;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=be991484079afe4510396a93d27bde7d237f55cc;hpb=2b5892c042136ebb0d9a2f773f3174c840ca0ba6;p=helm.git

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index be9914840..f03baa656 100644
--- a/matita/components/ng_tactics/nDestructTac.ml
+++ b/matita/components/ng_tactics/nDestructTac.ml
@@ -174,7 +174,7 @@ let hp_pattern_jm n =
 (* creates the discrimination = injection+contradiction principle *)
 exception ConstructorTooBig of string;;
 
-let mk_discriminator ~use_jmeq name it leftno status baseuri =
+let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri =
   let itnargs = 
     let _,_,arity,_ = it in 
     List.length (arg_list 0 arity) in
@@ -291,7 +291,7 @@ let mk_discriminator ~use_jmeq name it leftno status baseuri =
                  List.map
                    (fun i -> 
                       let nargs_kty = nargs it leftno i in
-                      if (nargs_kty > 5 && not use_jmeq) then raise (ConstructorTooBig (kname i)); 
+                      if (nargs_kty > 5 && not use_jmeq && not force) then raise (ConstructorTooBig (kname i)); 
                       let ts = iter (fun m acc -> mk_id ("t" ^ (string_of_int m))::acc)
                                  (nargs_kty - 1) [] in
                      let nones = 
@@ -321,11 +321,11 @@ let mk_discriminator ~use_jmeq name it leftno status baseuri =
   (* PHASE 2: create the object for the proof of the principle: we'll name it
    * "theorem" *)
   let status, theorem =
-   GrafiteDisambiguate.disambiguate_nobj status ~baseuri 
+   let attrs = `Generated, `Theorem, `DiscriminationPrinciple in
+   GrafiteDisambiguate.disambiguate_nobj status ~baseuri
     (baseuri ^ name ^ ".def",0,
       NotationPt.Theorem
-       (`Theorem,name,principle,
-         Some (NotationPt.Implicit (`Tagged "inv")),`DiscriminationPrinciple))
+       (name, principle, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
   in 
   let uri,height,nmenv,nsubst,nobj = theorem in
   let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
@@ -712,7 +712,9 @@ let rec destruct_tac0 tags acc domain skip status goal =
     let has_cleared = 
      try 
        let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
-     with _ -> true in
+     with 
+      | Sys.Break as e -> raise e
+      |_ -> true in
     let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
     let acc = rm_eq has_cleared acc in
     let skip = rm_eq has_cleared skip in
@@ -728,7 +730,9 @@ let rec destruct_tac0 tags acc domain skip status goal =
       let has_cleared = 
        try 
          let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
-       with _ -> true in
+       with 
+         | Sys.Break as e -> raise e         
+	 | _ -> true in
       let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
       let acc = rm_eq has_cleared acc in
       let skip = rm_eq has_cleared skip in