Skip to content

Commit 87dff37

Browse files
committed
Fix warnings in bootstrapped test file
1 parent eb17bf0 commit 87dff37

File tree

2 files changed

+2
-4
lines changed

2 files changed

+2
-4
lines changed

bootstrap/certicoqc/certicoqc_plugin_wrapper.ml

+1-4
Original file line numberDiff line numberDiff line change
@@ -77,10 +77,7 @@ let fix_term (p : Ast0.term) : Ast0.term =
7777
| Coq_tProj (p, t) -> Coq_tProj (p, aux t)
7878
| Coq_tFix (mfix, i) -> Coq_tFix (map aux_def mfix, i)
7979
| Coq_tCoFix (mfix, i) -> Coq_tCoFix (map aux_def mfix, i)
80-
| Coq_tInt i ->
81-
Printf.printf "Fixing prim int: %s\n" (Uint63.to_string i);
82-
Printf.printf "is_int? %b\n" (Obj.is_int (Obj.repr i));
83-
Coq_tInt i
80+
| Coq_tInt i -> Coq_tInt i
8481
| Coq_tFloat f -> Coq_tFloat f
8582
and aux_pred { puinst = puinst; pparams = pparams; pcontext = pcontext; preturn = preturn } =
8683
{ puinst; pparams = map aux pparams; pcontext; preturn = aux preturn }

bootstrap/certicoqc/test.v

+1
Original file line numberDiff line numberDiff line change
@@ -31,4 +31,5 @@ Definition certicoqc (opts : Options) (p : Template.Ast.Env.program) :=
3131
let () := coq_msg_info "certicoqc called" in
3232
compile opts p.
3333

34+
Set Warnings "-primitive-turned-into-axiom".
3435
Time CertiCoqC Compile -build_dir "tests" -time -O 1 certicoqc.

0 commit comments

Comments
 (0)