| Ast.LetRec (kind, definitions, term) ->
let definitions =
List.map
- (fun (var, ty, n) -> aux_capture_variable var, k ty, n)
+ (fun (params, var, ty, decrno) ->
+ List.map aux_capture_variable params, aux_capture_variable var,
+ k ty, decrno)
definitions
in
Ast.LetRec (kind, definitions, k term)
| Some term -> Some (k term)
and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
and aux_patterns patterns = List.map aux_pattern patterns
- and aux_pattern ((head, hrefs, vars), term) =
- ((head, hrefs, List.map aux_capture_variable vars), k term)
+ and aux_pattern =
+ function
+ Ast.Pattern (head, hrefs, vars), term ->
+ Ast.Pattern (head, hrefs, List.map aux_capture_variable vars), k term
+ | Ast.Wildcard, term -> Ast.Wildcard, k term
and aux_subst (name, term) = (name, k term)
and aux_substs substs = List.map aux_subst substs
in
and aux_branch (pattern, term) =
aux_pattern pattern ;
aux term
- and aux_pattern (head, _, vars) =
- List.iter aux_capture_var vars
- and aux_definition (var, term, i) =
+ and aux_pattern =
+ function
+ Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars
+ | Ast.Wildcard -> ()
+ and aux_definition (params, var, term, decrno) =
+ List.iter aux_capture_var params ;
aux_capture_var var ;
aux term
and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
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,i) -> (n,freshen_term t,b,i)) in
+ let freshen_capture_variables =
+ List.map (fun (n,t) -> (freshen_term n, HExtlib.map_option freshen_term t))
+ in
match obj with
| CicNotationPt.Inductive (params, indtypes) ->
let indtypes =
(fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors))
indtypes
in
- CicNotationPt.Inductive (freshen_name_ty params, indtypes)
+ CicNotationPt.Inductive (freshen_capture_variables params, indtypes)
| CicNotationPt.Theorem (flav, n, t, ty_opt) ->
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.Record (params, n, ty, fields) ->
- CicNotationPt.Record (freshen_name_ty params, n, freshen_term ty,
- freshen_name_ty_b fields)
+ CicNotationPt.Record (freshen_capture_variables params, n,
+ freshen_term ty, freshen_name_ty_b fields)
let freshen_term = freshen_term ?index:None