* metasenv as needed *)
val disambiguate :
disambiguator:MatitaTypes.disambiguator ->
- currentProof:MatitaTypes.currentProof ->
+ currentProof:#MatitaTypes.currentProof ->
DisambiguateTypes.term ->
DisambiguateTypes.environment * Cic.metasenv * Cic.term *
CicUniv.universe_graph
val get_context_and_metasenv:
- currentProof:MatitaTypes.currentProof ->
+ currentProof:#MatitaTypes.currentProof ->
Cic.context * Cic.metasenv