From 1f5dbcf7d5bc42583797b431927fdb2cb719246a Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Fri, 29 Mar 2024 12:04:47 +0100 Subject: [PATCH] add code to print logs in get_proof_data --- src/handle/command.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/handle/command.ml b/src/handle/command.ml index 32250959c..5ba340777 100644 --- a/src/handle/command.ml +++ b/src/handle/command.ml @@ -521,7 +521,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = (* Add the symbol in the signature. *) fst (Sig_state.add_symbol ss expo prop mstrat opaq p_sym_nam declpos a impl d) in - pdata_finalize_fct, fun() -> () + pdata_finalize_fct, fun() -> Console.out 2 (Color.red "symbol %a : %a") uid id term a | P_proof_end -> let pdata_finalize_fct ss ps = (* Check that the proof is indeed finished. *) @@ -535,7 +535,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = (* Add the symbol in the signature. *) fst (Sig_state.add_symbol ss expo prop mstrat opaq p_sym_nam declpos a impl d) in - pdata_finalize_fct, fun() -> () + pdata_finalize_fct, fun() -> Console.out 2 (Color.red "symbol %a : %a") uid id term a in (* Create the proof state. *)