add code to print logs in get_proof_data

Deducteam · Mar 29, 2024 · 1f5dbcf · 1f5dbcf
1 parent 95a3a29
commit 1f5dbcf
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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. *)