+ | Pt.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 compiled = compiler [p_some, 0] in
+ (fun term env ->
+ match compiled term with
+ | None -> Some none_env
+ | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
+ | _ -> assert false)