| [] -> assert false (* as above *)
| (name :: _) as names ->
let rec instantiate_fold_left acc env' =
- prerr_endline "instantiate_fold_left";
match lookup_value env' name with
| ListValue (_ :: _) ->
instantiate_fold_left
| [] -> assert false (* as above *)
| (name :: _) as names ->
let rec instantiate_fold_right env' =
- prerr_endline "instantiate_fold_right";
match lookup_value env' name with
| ListValue (_ :: _) ->
let acc = instantiate_fold_right (tail_names names env') in
| _ -> assert false
in
instantiate_fold_right env)
- | If (_, body)
- | Unless (_, body) -> aux env body
+ | If (_, p_true, p_false) as t -> aux env (CicNotationUtil.find_branch (Magic t))
+ | Fail -> assert false
| _ -> assert false
in
aux env term