diff options
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ab03f1831..72bb8253d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -106,12 +106,12 @@ let const_of_ref = function let nf_zeta env = Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) - env - Evd.empty + env (Evd.from_env env) let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty + Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env + (Evd.from_env Environ.empty_env) |