This patch allows generation of minimally dependent discrimination principles

[helm.git] / matita / components / grafite_engine / grafiteEngine.ml

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 5891698404d4661e9b4f83fa631b539f684f6055..15e20277f6f1ad5cb6d132c76686671f14512716 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -856,7 +856,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
           | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
         let (_,ind_name,_,_ as it) = List.nth tys indtyno in
         let status,obj =  
-          NDestructTac.mk_discriminator ~use_jmeq:true (ind_name ^ "_jmdiscr")
+          NDestructTac.mk_discriminator ~use_jmeq:true ~force:true (ind_name ^ "_jmdiscr")
            it leftno status status#baseuri in
         let _,_,menv,_,_ = obj in
           (match menv with