let get_constructors uri i =
let inductive_types =
- (match CicEnvironment.get_obj uri with
- Cic.Constant _ -> assert false
- | Cic.Variable _ -> assert false
- | Cic.CurrentProof _ -> assert false
- | Cic.InductiveDefinition (l,_,_) -> l
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o with
+ Cic.Constant _ -> assert false
+ | Cic.Variable _ -> assert false
+ | Cic.CurrentProof _ -> assert false
+ | Cic.InductiveDefinition (l,_,_) -> l
) in
let (_,_,_,constructors) = List.nth inductive_types i in
constructors
make_subst subst, Some uri_str)::List.map acic2cexpr tl))
| C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
let inductive_types =
- (match CicEnvironment.get_obj uri with
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
| Cic.CurrentProof _ -> assert false
make_subst subst, Some (UriManager.string_of_uri uri)))
| C.AMutInd (id,uri,i,subst) ->
let inductive_types =
- (match CicEnvironment.get_obj uri with
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
| Cic.CurrentProof _ -> assert false