| Env of (string * value_type) list
let make_action action bindings =
- let rec aux (vl : env_type) =
+ let rec aux (vl : CicNotationEnv.t) =
function
[] ->
prerr_endline "aux: make_action";
aux ((name, (ListType t, (ListValue v))) :: vl) tl)
| Env _ :: tl ->
prerr_endline "aux: env";
- Gramext.action (fun (v:env_type) -> aux (v @ vl) tl)
+ Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
(* LUCA: DEFCON 2 END *)
in
aux [] (List.rev bindings)
match magic with
| Opt p ->
let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
- let action (env_opt : env_type option) (loc : location) =
+ let action (env_opt : CicNotationEnv.t option) (loc : location) =
match env_opt with
| Some env -> List.map opt_binding_some env
| None -> List.map opt_binding_of_name p_names
(fun env (n, (_, v)) -> grow_env_entry env n v)
env env_i
in
- let action (env_list : env_type list) (loc : location) =
+ let action (env_list : CicNotationEnv.t list) (loc : location) =
prerr_endline "list action";
List.fold_right grow_env env_list env0
in
let p_names = flatten_opt p_bindings in
let _ = prerr_endline ("inner names: " ^ String.concat " " (List.map fst p_names)) in
let action =
- make_action (fun (env : env_type) (loc : location) -> prerr_endline "inner action"; env) p_bindings
+ make_action (fun (env : CicNotationEnv.t) (loc : location) -> env)
+ p_bindings
in
p_bindings, p_atoms, p_names, action
in
associativity,
[ p_atoms,
(make_action
- (fun (env: env_type) (loc: location) -> (action env loc))
+ (fun (env: CicNotationEnv.t) (loc: location) -> (action env loc))
p_bindings) ]]]
in
p_atoms