Write a tactic to discharge integer literal proof obligations

1 files changed, 1 insertions, 1 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 6bda6376..9496fcf9 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -573,7 +573,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             F.pp_print_string fmt (int_name sv.int_ty);
             F.pp_print_string fmt ".ofNatCore ";
             Z.pp_print fmt sv.value;
-            F.pp_print_string fmt (" (by simp))"))
+            F.pp_print_string fmt (" (by intlit))"))
     | Bool b ->
         let b = if b then "true" else "false" in
         F.pp_print_string fmt b