diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 index ea31101..7a2a473 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 @@ -4682,11 +4682,9 @@ let rec strip_unfold_term env ((sigma, t) as p) kt = match kind_of_term t with then strip_unfold_term env (sigma, f) kt else (sigma, f), true | Const (c,_) when Environ.is_projection c env -> - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma ((ty,_), sigma, _) = + let sigma, (ty, _) = Evarutil.new_type_evar env sigma (Evd.UnivFlexible true) in - let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma ty in - let sigma = Sigma.to_evar_map sigma in + let sigma, ev = Evarutil.new_evar env sigma ty in (sigma, mkProj(Projection.make c false, ev)), true | Const _ | Var _ -> p, true | Proj _ -> p, true |