From: Claudio Sacerdoti Coen Date: Thu, 30 Aug 2012 08:22:05 +0000 (+0000) Subject: Composite coercions are now extracted too. X-Git-Tag: make_still_working~1513 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=abed266f42c25bf77c5c4bfbff0450abe9680e7a;p=helm.git Composite coercions are now extracted too. --- diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index d61ad6103..589169840 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);