From ce87c17955727a7c2a0178a635c4bd17edd4252c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 25 Aug 2020 18:36:19 +0100
Subject: Coq: Use proof mode for a couple of Fixpoints to avoid Coq 8.12 issue

---
 lib/coq/Values.v | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Values.v b/lib/coq/Values.v
index 4b48151a..0119711a 100644
--- a/lib/coq/Values.v
+++ b/lib/coq/Values.v
@@ -2548,21 +2548,30 @@ Fixpoint foreach_Z' {Vars} from to step n (vars : Vars) (body : Z -> Vars -> Var
 Definition foreach_Z {Vars} from to step vars body :=
   foreach_Z' (Vars := Vars) from to step (S (Z.abs_nat (from - to))) vars body.
 
-Fixpoint foreach_Z_up' {Vars} (from to step off : Z) (n:nat) `{ArithFact (0 <? step)} `{ArithFact (0 <=? off)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((from <=? z <=? to))), Vars -> Vars) {struct n} : Vars :=
+(* Define these in proof mode to avoid anomalies related to abstract.
+   (See https://github.com/coq/coq/issues/10959) *)
+
+Fixpoint foreach_Z_up' {Vars} (from to step off : Z) (n:nat) `{ArithFact (0 <? step)} `{ArithFact (0 <=? off)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((from <=? z <=? to))), Vars -> Vars) {struct n} : Vars.
+refine (
   if sumbool_of_bool (from + off <=? to) then
     match n with
     | O => vars
-    | S n => let vars := body (from + off) _ vars in foreach_Z_up' from to step (off + step) n vars body
+    | S n => let vars := body (from + off) _ vars in foreach_Z_up' _ from to step (off + step) n _ _ vars body
     end
-  else vars.
+  else vars
+).
+Defined.
 
-Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (0 <? step)} `{ArithFact (off <=? 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((to <=? z <=? from))), Vars -> Vars) {struct n} : Vars :=
+Fixpoint foreach_Z_down' {Vars} from to step off (n:nat) `{ArithFact (0 <? step)} `{ArithFact (off <=? 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((to <=? z <=? from))), Vars -> Vars) {struct n} : Vars.
+refine (
   if sumbool_of_bool (to <=? from + off) then
     match n with
     | O => vars
-    | S n => let vars := body (from + off) _ vars in foreach_Z_down' from to step (off - step) n vars body
+    | S n => let vars := body (from + off) _ vars in foreach_Z_down' _ from to step (off - step) n _ _ vars body
     end
-  else vars.
+  else vars
+).
+Defined.
 
 Definition foreach_Z_up {Vars} from to step vars body `{ArithFact (0 <? step)} :=
     foreach_Z_up' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
-- 
cgit v1.2.3