match cic with
| Cic.Const (uri, []) ->
let uris =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
(*match CicTypeChecker.typecheck uri with*)
| Cic.Constant (_, _, _, uris) -> uris
Cic.Const (uri, mk_subst uris)
| Cic.Var (uri, []) ->
let uris =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
(*match CicTypeChecker.typecheck uri with*)
| Cic.Variable (_, _, _, uris) -> uris
Cic.Var (uri, mk_subst uris)
| Cic.MutInd (uri, i, []) ->
let uris =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
(*match CicTypeChecker.typecheck uri with*)
| Cic.InductiveDefinition (_, uris, _) -> uris
Cic.MutInd (uri, i, mk_subst uris)
| Cic.MutConstruct (uri, i, j, []) ->
let uris =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
(*match CicTypeChecker.typecheck uri with*)
| Cic.InductiveDefinition (_, uris, _) -> uris