X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2Facic2content.ml;h=23d6447863a9f9335f101d240e1edfa51ca885dd;hb=213cc7cf3c9da7c024b44b54e07035b831f7a31f;hp=e72d466d537fb7724dd91daadbe99f0886dee46f;hpb=9e5abfcf937cb4fa85387cbd2b6503c2bf21a32c;p=helm.git

diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml
index e72d466d5..23d644786 100644
--- a/components/acic_content/acic2content.ml
+++ b/components/acic_content/acic2content.ml
@@ -44,6 +44,8 @@ let conclude_prefix = "concl:";;
 let premise_prefix = "prem:";;
 let lemma_prefix = "lemma:";;
 
+let hide_coercions = ref true;;
+
 (* e se mettessi la conversione di BY nell'apply_context ? *)
 (* sarebbe carino avere l'invariante che la proof2pres
 generasse sempre prove con contesto vuoto *)
@@ -500,13 +502,16 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
           generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
         else raise Not_a_proof 
     | C.AAppl (id,li) ->
-        (try rewrite 
+        (try coercion 
+           seed li ~ids_to_inner_types ~ids_to_inner_sorts
+         with NotApplicable ->
+         try rewrite 
            seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
          try inductive 
           seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
-	 try transitivity 
+         try transitivity 
            seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
           let subproofs, args =
@@ -795,6 +800,22 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           } 
   | _ -> raise NotApplicable
 
+and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
+  match li with
+    | ((Cic.AConst _) as he)::tl
+    | ((Cic.AMutInd _) as he)::tl
+    | ((Cic.AMutConstruct _) as he)::tl when 
+       CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
+       !hide_coercions ->
+        let rec last =
+         function
+            [] -> assert false
+          | [t] -> t
+          | _::tl -> last tl
+        in
+          acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+    | _ -> raise NotApplicable
+
 and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
   let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
   let module C2A = Cic2acic in