(* {{{ parser initialization *)
EXTEND
GLOBAL: term statement;
- constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
+ constructor: [
+ [ name = IDENT; params = LIST0 protected_binder_vars; SYMBOL ":"; typ = term -> (* FG: params added *)
+ (name, shift_params `Forall params typ)
+ ]
+ ];
tactic_term: [ [ t = term LEVEL "90" -> t ] ];
ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ];
nreduction_kind: [
params = LIST0 protected_binder_vars;
SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
fields = LIST0 [
- name = IDENT ;
+ name = IDENT ;
+ params = LIST0 protected_binder_vars; (* FG: params added *)
coercion = [
SYMBOL ":" -> false,0
| SYMBOL ":"; SYMBOL ">" -> true,0
| SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
];
ty = term ->
- let b,n = coercion in
- (name,ty,b,n)
+ let b,n = coercion in
+ (name, shift_params `Forall params ty, b, n)
] SEP SYMBOL ";"; SYMBOL "}" ->
let params =
List.fold_right