| Ast.Default (p_some, p_none) -> (* p_none can't bound names *)
let p_some_decls = Env.declarations_of_term p_some in
- let none_env = List.map Env.opt_binding_of_name p_some_decls in
+ let p_none_decls = Env.declarations_of_term p_none in
+ let p_opt_decls =
+ List.filter
+ (fun decl -> not (List.mem decl p_none_decls))
+ p_some_decls
+ in
+ let none_env = List.map Env.opt_binding_of_name p_opt_decls in
let compiled = compiler [p_some, 0] in
(fun term env ->
match compiled term with
| None -> Some none_env (* LUCA: @ env ??? *)
- | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
+ | Some (env', 0) ->
+ let env' =
+ List.map
+ (fun (name, (ty, v)) as binding ->
+ if List.exists (fun (name', _) -> name = name') p_opt_decls
+ then Env.opt_binding_some binding
+ else binding)
+ env'
+ in
+ Some (env' @ env)
| _ -> assert false)
| Ast.If (p_test, p_true, p_false) ->