Commit 249ec851 authored by MARCHE Claude's avatar MARCHE Claude

No need to reverse the result of split_theory anymore

parent ab24d4f9
......@@ -1592,7 +1592,7 @@ let make_theory_section ?merge ~detached (s:session) parent_name (th:Theory.theo
mk_proof_node ~version:s.session_shape_version ~expl
s name task parent id;
let tasks = List.rev (Task.split_theory th None None) in
let tasks = Task.split_theory th None None in
let goalsID = (fun _ -> gen_proofNodeID s) tasks in
let theory = { theory_name = th.Theory.th_name;
theory_checksum = None;
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment