Commit bc8f514c authored by MARCHE Claude's avatar MARCHE Claude
Browse files

continued

parent 504c6ffb
......@@ -557,7 +557,6 @@ let split_unproved_goals () =
subgoals = [];
}
in
List.iter (fun t -> eprintf "%a@." Pretty.print_task t) subgoals;
goals_model#set ~row:split_row ~column:Model.index_column
(Model.Row_transformation tr);
g.Model.transformations <- tr :: g.Model.transformations;
......
......@@ -33,7 +33,7 @@ let split_case spl c acc tl bl =
let bll,_ = List.fold_left (fun (bll,el) (pl,f) ->
let spf = spl [] f in
let brc = f_close_branch pl c in
let bll = List.rev_map (fun rl -> brc::rl) bll in
let bll = List.map (fun rl -> brc::rl) bll in
let bll = apply_append (fun f -> f_close_branch pl f :: el) bll spf in
bll, brc::el) ([],[]) bl
in
......
......@@ -61,3 +61,19 @@ theory TestFloat
end
theory TestList
use import int.Int
use import list.List
logic x : list int
goal Test1:
match x with
| Nil -> 1 = 0 /\ 2 = 3
| Cons _ Nil -> 4 = 5 and 6 = 7
| Cons _ _ -> 8 = 9 /\ 10 = 11
end
end
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment