From 41916775e9f68ddfa78040a803a2426415137c94 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 6 Dec 2016 15:36:10 +0100
Subject: Use Tacred.unfoldn [AllOccurrences..] to work around Coq #5250

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 +-
 mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4  | 2 +-
 mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4  | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/ssreflect/plugin')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index a41da9a..39fe3d6 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -4752,7 +4752,7 @@ let unfoldintac occ rdx t (kt,_) gl =
   let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
   let (sigma, t), const = strip_unfold_term env0 t kt in
   let body env t c =
-    Tacred.unfoldn [OnlyOccurrences [1], get_evalref t] env sigma0 c in
+    Tacred.unfoldn [AllOccurrences, get_evalref t] env sigma0 c in
   let easy = occ = None && rdx = None in
   let red_flags = if easy then CClosure.betaiotazeta else CClosure.betaiota in
   let beta env = Reductionops.clos_norm_flags red_flags env sigma0 in
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index accb7b5..ea31101 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -4702,7 +4702,7 @@ let unfoldintac occ rdx t (kt,_) gl =
   let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
   let (sigma, t), const = strip_unfold_term env0 t kt in
   let body env t c =
-    Tacred.unfoldn [OnlyOccurrences [1], get_evalref t] env sigma0 c in
+    Tacred.unfoldn [AllOccurrences, get_evalref t] env sigma0 c in
   let easy = occ = None && rdx = None in
   let red_flags = if easy then Closure.betaiotazeta else Closure.betaiota in
   let beta env = Reductionops.clos_norm_flags red_flags env sigma0 in
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4
index d575a4f..25d3287 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4
@@ -4755,7 +4755,7 @@ let unfoldintac occ rdx t (kt,_) gl =
   let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
   let (sigma, t), const = strip_unfold_term env0 t kt in
   let body env t c =
-    Tacred.unfoldn [OnlyOccurrences [1], get_evalref t] env sigma0 c in
+    Tacred.unfoldn [AllOccurrences, get_evalref t] env sigma0 c in
   let easy = occ = None && rdx = None in
   let red_flags = if easy then CClosure.betaiotazeta else CClosure.betaiota in
   let beta env = Reductionops.clos_norm_flags red_flags env sigma0 in
-- 
cgit v1.2.3