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