Commit 929ff27d authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

stared rework interactive.ml for passage to double continuation style

parent 5f143c27
Pipeline #1648 passed with stage
in 3 minutes and 4 seconds
This diff is collapsed.
......@@ -102,7 +102,7 @@ let main_interactive () =
back_track = Root;
node_type = User })
formula_list in
ignore(interactive_proof (new_interactive_state param proof_list));;
ignore(interactive_proof (new_state param proof_list));;
(**********************)
......@@ -110,7 +110,7 @@ let main_interactive () =
(**********************)
(* Create and set-up a dummy state and environment for testing. *)
let test_state = dummy_interactive_state ();;
let test_state = dummy_state ();;
let env =
let env = test_state.c_proof.goal.env in
......
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