context:Cic.context ->
metasenv:Cic.metasenv ->
?initial_ugraph:CicUniv.universe_graph ->
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
DisambiguateTypes.term ->
context:Cic.context ->
metasenv:Cic.metasenv ->
?initial_ugraph:CicUniv.universe_graph ->
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
DisambiguateTypes.term ->