| Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
| Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
| Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
- | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
+ | Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u))
| Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput
| Cic.AImplicit (id, _) -> idref id Ast.Implicit
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
| `Set | `Type _ -> `Pi
- | `Prop | `CProp -> `Forall
+ | `Prop | `CProp _ -> `Forall
in
idref id (Ast.Binder (binder_kind,
(CicNotationUtil.name_of_cic_name n, Some (k s)), k t))