X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=15e20277f6f1ad5cb6d132c76686671f14512716;hb=3d981fb10ebc350bc3fc693f0a433d51fc35715a;hp=d61ad61039dc54f450067d8e5be6c5f452bf4dde;hpb=210b6e113724900dd5c5745da2881b868154d241;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index d61ad6103..15e20277f 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -776,6 +776,13 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
                       status (name,true,t,cpos,arity) in
                  let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
+                 let status =
+                  List.fold_left
+                   (fun status uri ->
+                     let obj = NCicEnvironment.get_checked_obj status uri in
+                      eval_extract_obj status obj
+                   ) status nuris
+                 in
                   eval_alias status (mode,aliases)
                with MultiPassDisambiguator.DisambiguationError _-> 
                  HLog.warn ("error in generating coercion: "^name);
@@ -849,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