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
}
| _ -> 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 =