else
(* We are already in an inner-type and Coscoy's double *)
(* type inference algorithm has not been applied. *)
else
(* We are already in an inner-type and Coscoy's double *)
(* type inference algorithm has not been applied. *)
match binding with
Some (n,Cic.Def (t,_)) ->
let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
match binding with
Some (n,Cic.Def (t,_)) ->
let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
(binding::context),
((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
| Some (n,Cic.Decl t) ->
let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
(binding::context),
((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
| Some (n,Cic.Decl t) ->
let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
(binding::context),
((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs)
| None ->
(binding::context),
((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs)
| None ->