X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnDestructTac.ml;h=fdee9e12713a103b5fea02848b3ce5ffb48d7745;hb=fd12cbee622c58bc45089d62c3e6f131c238beb5;hp=990cc672bbede15aaa17f8f9a2a088e8c452319e;hpb=5ac2dc4e01aca542ddd13c02b304c646d8df9799;p=helm.git

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index 990cc672b..fdee9e127 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 =