Patch to add a debugging string to HExtlib.split_nth reverted

[helm.git] / helm / software / components / acic_content / acic2content.ml

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index b1423c5ab8cd805670fe4817fcf538c05ebb4107..c8ff783c3eafab71d645e5bc13005682259a62ae 100644 (file)
--- 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 =