From abed266f42c25bf77c5c4bfbff0450abe9680e7a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Aug 2012 08:22:05 +0000
Subject: [PATCH] Composite coercions are now extracted too.
---
matita/components/grafite_engine/grafiteEngine.ml | 7 +++++++
1 file changed, 7 insertions(+)
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);
--
2.39.5