From 6bfad00208b0385fbe49ec4b2ea1991930ef8816 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 6 Sep 2024 17:38:30 +0200
Subject: [PATCH] Adapt to coq/coq#18939 (Unification Firstorder Function
 Conversion off)

---
 BigN/Nbasic.v             | 4 ++--
 BigN/gen/NMake_gen.ml     | 9 +++++----
 CyclicDouble/DoubleBase.v | 7 ++++---
 3 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/BigN/Nbasic.v b/BigN/Nbasic.v
index 5e90137..aa70e7e 100644
--- a/BigN/Nbasic.v
+++ b/BigN/Nbasic.v
@@ -322,8 +322,8 @@ Section CompareRec.
  Lemma spec_compare0_mn: forall n x,
    compare0_mn n x = (0 ?= double_to_Z n x).
  Proof.
-  intros n; elim n; clear n; auto.
-  intros x; rewrite spec_compare0_m; rewrite w_to_Z_0; auto.
+  intros n; elim n; clear n.
+  { intros. rewrite w_to_Z_0 in spec_compare0_m. exact (spec_compare0_m x). }
   intros n Hrec x; case x; unfold compare0_mn; fold compare0_mn; auto.
   fold word in *.
   intros xh xl.
diff --git a/BigN/gen/NMake_gen.ml b/BigN/gen/NMake_gen.ml
index e89e17b..ba82e84 100644
--- a/BigN/gen/NMake_gen.ml
+++ b/BigN/gen/NMake_gen.ml
@@ -994,7 +994,7 @@ pr "
   inversion LT |
   subst; change (reduce 0 x = red_t 0 x); reflexivity |
   specialize (H (pred n)); subst; destruct x;
-   [|unfold_red; rewrite H; auto]; reflexivity
+   [|unfold_red; simpl in H; rewrite H; auto]; reflexivity
  ].
 
  Lemma reduce_equiv : forall n x, n <= Size -> reduce n x = red_t n x.
@@ -1006,9 +1006,10 @@ pr "
  Lemma spec_reduce_n : forall n x, [reduce_n n x] = [Nn n x].
  Proof.
  assert (H : forall x, reduce_%i x = red_t (SizePlus 1) x).
-  destruct x; [|unfold reduce_%i; rewrite (reduce_equiv Size)]; auto.
+  (* we have to [change] even though we declared equivalent keys... *)
+  destruct x; [|unfold reduce_%i; change reduce_%i with (reduce %i); rewrite (reduce_equiv Size)]; auto.
  induction n.
-   intros. rewrite H. apply spec_red_t.
+   intros. simpl. rewrite H. apply spec_red_t.
  destruct x as [|xh xl].
  simpl. rewrite make_op_S. exact ZnZ.spec_0.
  fold word in *.
@@ -1017,7 +1018,7 @@ pr "
  rewrite IHn.
  rewrite spec_extend_WW; auto.
  Qed.
-" (size+1) (size+1);
+" (size+1) (size+1) size size;
 
 pr
 " Lemma spec_reduce : forall n x, [reduce n x] = ZnZ.to_Z x.
diff --git a/CyclicDouble/DoubleBase.v b/CyclicDouble/DoubleBase.v
index 3959a98..541a3da 100644
--- a/CyclicDouble/DoubleBase.v
+++ b/CyclicDouble/DoubleBase.v
@@ -367,9 +367,10 @@ Section DoubleBase.
   Lemma spec_double_WW : forall n (h l : word w n),
     [!S n|double_WW n h l!] = [!n|h!] * double_wB n + [!n|l!].
   Proof.
-   induction n;simpl;intros;trivial.
-   destruct h;auto.
-   destruct l;auto.
+   induction n;simpl;intros.
+   - unfold ww_to_Z in spec_w_WW; trivial.
+   - destruct h;auto.
+     destruct l;auto.
   Qed.
 
   Lemma spec_extend_aux : forall n x, [!S n|extend_aux n x!] = [[x]].