raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
) branches
else
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
Cic.InductiveDefinition (il,_,leftsno,_) ->
let _,_,_,cl =
try
(try
match cic with
| Cic.Const (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.Const (uri, mk_subst uris)
| Cic.Var (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.Var (uri, mk_subst uris)
| Cic.MutInd (uri, i, []) ->
(try
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.MutInd (uri, i, mk_subst uris)
with
(*here the explicit_named_substituion is assumed to be of length 0 *)
Cic.MutInd (uri,i,[]))
| Cic.MutConstruct (uri, i, j, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.MutConstruct (uri, i, j, mk_subst uris)
| Cic.Meta _ | Cic.Implicit _ as t ->
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
let disambiguate_thing ~dbd ~context ~metasenv
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
+ ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
(thing_txt,thing_txt_prefix_len,thing)
=
failwith "Disambiguate: circular dependency"
let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
+ ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
(text,prefix_len,term)
=
let term =