X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2Facic2content.ml;h=c8ff783c3eafab71d645e5bc13005682259a62ae;hb=910c252965fe17d6b5af92e4658e7d02bac82d58;hp=b1423c5ab8cd805670fe4817fcf538c05ebb4107;hpb=790eccfa6b94dc82826d919691f8d4bfadb04573;p=helm.git

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index b1423c5ab..c8ff783c3 100644
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -561,7 +561,7 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t
           raise Not_a_proof
     | C.AAppl (id,li) ->
         (try coercion 
-           seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts
+           seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
          try rewrite 
            seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
@@ -885,21 +885,31 @@ and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner
           } 
   | _ -> raise NotApplicable
 
-and coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts =
+and coercion seed context metasenv id 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 
-       CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
-       !hide_coercions ->
-        let rec last =
-         function
-            [] -> assert false
-          | [t] -> t
-          | _::tl -> last tl
+       (match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+       | None -> false | Some (_,_,_,_,cpos) -> cpos < List.length tl)
+       && !hide_coercions ->
+        let cpos,sats =
+          match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+          | None -> assert false
+          | Some (_,_,_,sats,cpos) -> cpos, sats
         in
-          acic2content 
-            seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+        let x = List.nth tl cpos in
+        let _,rest = 
+          try HExtlib.split_nth (cpos + sats +1) tl with Failure _ -> [],[] 
+        in
+        if rest = [] then
+         acic2content 
+          seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts 
+           x
+        else
+         acic2content 
+          seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts 
+           (Cic.AAppl (id,x::rest))
     | _ -> raise NotApplicable
 
 and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =