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/trunk | |
| parent | bcfeaf7951c0cbd9fa950b4ce67206451a17defb (diff) | |
Use Tacred.unfoldn [AllOccurrences..] to work around Coq #5250
Diffstat (limited to 'mathcomp/ssreflect/plugin/trunk')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 |
1 files changed, 1 insertions, 1 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 |