Commit 04598b1d authored by Adrien Koutsos's avatar Adrien Koutsos

minor

parent 02862184
Pipeline #2009 passed with stage
in 1 minute and 31 seconds
...@@ -885,7 +885,7 @@ let euf_need_to_guard t t' g_data = ...@@ -885,7 +885,7 @@ let euf_need_to_guard t t' g_data =
(subterm g_data.left_guard.term t) (subterm g_data.left_guard.term t)
|| (subterm g_data.right_guard.term t') || (subterm g_data.right_guard.term t')
(* auto_guard state sk fk : Try to guard all decryption pairs possible. *) (* euf_auto_guard state sk fk : Try to guard all decryption pairs possible. *)
let euf_auto_guard side b state sk fk = let euf_auto_guard side b state sk fk =
let goal = state.c_proof.goal in let goal = state.c_proof.goal in
let env = goal.env in let env = goal.env in
...@@ -1018,7 +1018,7 @@ let cca_make_guard_data goal enc_pairs t t' = ...@@ -1018,7 +1018,7 @@ let cca_make_guard_data goal enc_pairs t t' =
(* auto_guard state sk fk : Try to guard all decryption pairs possible. *) (* cca_auto_guard state sk fk : Try to guard all decryption pairs possible. *)
let cca_auto_guard state sk fk = let cca_auto_guard state sk fk =
let goal = state.c_proof.goal in let goal = state.c_proof.goal in
let env = goal.env in let env = 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