diff options
| author | Enrico Tassi | 2016-12-06 15:36:10 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2016-12-06 16:31:01 +0100 |
| commit | 41916775e9f68ddfa78040a803a2426415137c94 (patch) | |
| tree | 7788645f7583fc124844ca51df96a5f2fff58475 /mathcomp/ssreflect/plugin | |
| parent | bcfeaf7951c0cbd9fa950b4ce67206451a17defb (diff) | |
Use Tacred.unfoldn [AllOccurrences..] to work around Coq #5250
Diffstat (limited to 'mathcomp/ssreflect/plugin')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4 | 2 |
3 files changed, 3 insertions, 3 deletions
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 |