CicEnvironment.CircularDependency _ ->
raise DisambiguateChoices.Invalid_choice))
| CicAst.Implicit -> Cic.Implicit None
CicEnvironment.CircularDependency _ ->
raise DisambiguateChoices.Invalid_choice))
| CicAst.Implicit -> Cic.Implicit None
| CicAst.Num (num, i) -> resolve env (Num i) ~num ()
| CicAst.Meta (index, subst) ->
let cic_subst =
| CicAst.Num (num, i) -> resolve env (Num i) ~num ()
| CicAst.Meta (index, subst) ->
let cic_subst =
| CicAst.Sort `CProp -> Cic.Sort Cic.CProp
| CicAst.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
| CicAst.Sort `CProp -> Cic.Sort Cic.CProp
| CicAst.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
and aux_option loc context = function
| None -> Cic.Implicit (Some `Type)
| Some term -> aux loc context term
and aux_option loc context = function
| None -> Cic.Implicit (Some `Type)
| Some term -> aux loc context term