| Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
| Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u))
| Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput
| Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
| Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u))
| Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
else
idref aid (Ast.Appl (List.map k args)))
| Cic.AAppl (aid,args) ->
else
idref aid (Ast.Appl (List.map k args)))
| Cic.AAppl (aid,args) ->
| Ast.ImplicitPattern -> mk_implicit false
| Ast.VarPattern name -> lookup name
| Ast.ApplPattern terms -> mk_appl (List.map aux terms)
| Ast.ImplicitPattern -> mk_implicit false
| Ast.VarPattern name -> lookup name
| Ast.ApplPattern terms -> mk_appl (List.map aux terms)