* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
module Ast = CicNotationPt
let visit_ast ?(special_k = fun _ -> assert false) k =
let index = ref 0 in
let freshen_term = freshen_term ~index in
let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
+ let freshen_name_ty_b = List.map (fun (n, t, b) -> (n, freshen_term t, b)) in
match obj with
| CicNotationPt.Inductive (params, indtypes) ->
let indtypes =
CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
| CicNotationPt.Record (params, n, ty, fields) ->
CicNotationPt.Record (freshen_name_ty params, n, freshen_term ty,
- freshen_name_ty fields)
+ freshen_name_ty_b fields)
let freshen_term = freshen_term ?index:None