From dee74ca1f90acb076289286f6f69df65e63604ce Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Mon, 23 Jan 2023 18:43:45 -0800
Subject: Write a tactic to discharge integer literal proof obligations

---
 compiler/Extract.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler')

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
-- 
cgit v1.2.3