| Ast.Variable _) as t -> special_k t
| (Ast.Ident _
| Ast.NRef _
- | Ast.Implicit
+ | Ast.NCic _
+ | Ast.Implicit _
| Ast.Num _
| Ast.Sort _
| Ast.Symbol _
| Ast.Ident (_, Some substs) -> aux_substs substs
| Ast.Meta (_, substs) -> aux_meta_substs substs
- | Ast.Implicit
+ | Ast.Implicit _
| Ast.Ident _
| Ast.Num _
| Ast.Sort _
indtypes
in
CicNotationPt.Inductive (freshen_capture_variables params, indtypes)
- | CicNotationPt.Theorem (flav, n, t, ty_opt) ->
+ | CicNotationPt.Theorem (flav, n, t, ty_opt,p) ->
let ty_opt =
match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
in
- CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
+ CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
| CicNotationPt.Record (params, n, ty, fields) ->
CicNotationPt.Record (freshen_capture_variables params, n,
freshen_term ty, freshen_name_ty_b fields)