From 87dff37df58f426fa0c267ac45908f0ce40e7b17 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Wed, 12 Oct 2022 00:18:33 +0200
Subject: [PATCH] Fix warnings in bootstrapped test file

---
 bootstrap/certicoqc/certicoqc_plugin_wrapper.ml | 5 +----
 bootstrap/certicoqc/test.v                      | 1 +
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml b/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml
index 70e32ebe..f2381754 100644
--- a/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml
+++ b/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml
@@ -77,10 +77,7 @@ let fix_term (p : Ast0.term) : Ast0.term =
   | Coq_tProj (p, t) -> Coq_tProj (p, aux t)
   | Coq_tFix (mfix, i) -> Coq_tFix (map aux_def mfix, i)
   | Coq_tCoFix (mfix, i) -> Coq_tCoFix (map aux_def mfix, i)
-  | Coq_tInt i ->
-    Printf.printf "Fixing prim int: %s\n" (Uint63.to_string i);
-    Printf.printf "is_int? %b\n" (Obj.is_int (Obj.repr i));
-    Coq_tInt i
+  | Coq_tInt i -> Coq_tInt i
   | Coq_tFloat f -> Coq_tFloat f
   and aux_pred { puinst = puinst; pparams = pparams; pcontext = pcontext; preturn = preturn } =
     { puinst; pparams = map aux pparams; pcontext; preturn = aux preturn }
diff --git a/bootstrap/certicoqc/test.v b/bootstrap/certicoqc/test.v
index 6044b4cf..ec404bda 100644
--- a/bootstrap/certicoqc/test.v
+++ b/bootstrap/certicoqc/test.v
@@ -31,4 +31,5 @@ Definition certicoqc (opts : Options) (p : Template.Ast.Env.program) :=
   let () := coq_msg_info "certicoqc called" in
   compile opts p.
 
+Set Warnings "-primitive-turned-into-axiom".
 Time CertiCoqC Compile -build_dir "tests" -time -O 1 certicoqc.