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 b10464bdad1acd6133dd117709e9221f0be55b12..c8ff783c3eafab71d645e5bc13005682259a62ae 100644 (file)
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -427,7 +427,7 @@ let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_
                  if sort = `Prop then 
                     let inductive_types =
                       (let o,_ = 
-                        CicEnvironment.get_obj CicUniv.empty_ugraph uri
+                        CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
                       in
                         match o with 
                           | Cic.InductiveDefinition (l,_,_,_) -> l 
@@ -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
@@ -612,7 +612,7 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
         let inductive_types,noparams =
-          (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+          (let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
             match o with
                 Cic.Constant _ -> assert false
                | Cic.Variable _ -> assert false
@@ -780,7 +780,7 @@ and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner
         let ind_str = (prefix ^ ".ind") in 
         let ind_uri = UriManager.uri_of_string ind_str in
         let inductive_types,noparams =
-          (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
+          (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ind_uri in
             match o with
                | Cic.InductiveDefinition (l,_,n,_) -> (l,n) 
                | _ -> assert false
@@ -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 =