From 100d14e136e354311c0f9ee6f10524fabbcf27d9 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 5 Feb 2025 13:41:54 +0100
Subject: [PATCH] derive.eqb currently broken on int63

---
 apps/derive/tests/test_eqbOK.v           |  2 +-
 apps/derive/tests/test_eqbcorrect.v      |  2 +-
 apps/derive/theories/derive/eqbcorrect.v | 12 +++++++-----
 3 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/apps/derive/tests/test_eqbOK.v b/apps/derive/tests/test_eqbOK.v
index 1db6f062b..5b9b9c151 100644
--- a/apps/derive/tests/test_eqbOK.v
+++ b/apps/derive/tests/test_eqbOK.v
@@ -30,7 +30,7 @@ Fail Elpi derive.eqbOK iota.
 (*
 Elpi derive.eqbOK large.
 *)
-Elpi derive.eqbOK prim_int.
+(* Elpi derive.eqbOK prim_int. *)
 Fail Elpi derive.eqbOK prim_float.
 Elpi derive.eqbOK fo_record.
 Elpi derive.eqbOK pa_record.
diff --git a/apps/derive/tests/test_eqbcorrect.v b/apps/derive/tests/test_eqbcorrect.v
index fabb3a5b8..1d3962d4b 100644
--- a/apps/derive/tests/test_eqbcorrect.v
+++ b/apps/derive/tests/test_eqbcorrect.v
@@ -35,7 +35,7 @@ Fail Elpi derive.eqbcorrect iota.
 (*
 Elpi derive.eqbcorrect large.
 *)
-Elpi derive.eqbcorrect prim_int.
+(* Elpi derive.eqbcorrect prim_int. *)
 Fail Elpi derive.eqbcorrect prim_float. (* Can not work, we don't have a syntaxtic test *)
 Elpi derive.eqbcorrect fo_record.
 Elpi derive.eqbcorrect pa_record.
diff --git a/apps/derive/theories/derive/eqbcorrect.v b/apps/derive/theories/derive/eqbcorrect.v
index fc2c7bbf5..e945fdaf5 100644
--- a/apps/derive/theories/derive/eqbcorrect.v
+++ b/apps/derive/theories/derive/eqbcorrect.v
@@ -35,6 +35,7 @@ Ltac eqb_refl_on__solver :=
   repeat ((apply /andP; split) || reflexivity || assumption).
 End exports.
 
+(*
 Require Import Uint63Axioms.
 
 Lemma uint63_eqb_correct i : eqb_correct_on PrimInt63.eqb i.
@@ -42,6 +43,7 @@ Proof. exact: eqb_correct. Qed.
 
 Lemma uint63_eqb_refl i : eqb_refl_on PrimInt63.eqb i.
 Proof. exact: eqb_refl. Qed.
+*)
 
 Elpi Db derive.eqbcorrect.db lp:{{
 
@@ -50,17 +52,17 @@ Elpi Db derive.eqbcorrect.db lp:{{
     o:constant, % correct
     o:constant. % reflexive
   
-  eqcorrect-for {{:gref PrimInt63.int }} C R :-
-    {{:gref uint63_eqb_correct}} = const C,
-    {{:gref uint63_eqb_refl}} = const R.
+%  eqcorrect-for {{:gref PrimInt63.int }} C R :-
+%    {{:gref uint63_eqb_correct}} = const C,
+%    {{:gref uint63_eqb_refl}} = const R.
 
   :index(2)
   pred correct-lemma-for i:term, o:term.
-  correct-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_correct }}.
+%  correct-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_correct }}.
 
   :index(2)
   pred refl-lemma-for i:term, o:term.
-  refl-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_refl }}.
+%  refl-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_refl }}.
 
 }}.