(* 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
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 =