val destruct_tac : string list option -> string list -> 's NTacStatus.tactic
-val mk_discriminator: (use_jmeq: bool) ->
+val mk_discriminator: (use_jmeq: bool) -> ?force:bool ->
string -> NCic.inductiveType -> int ->
(#NTacStatus.tac_status as 's) -> string -> 's * NCic.obj