diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-05-03 17:44:34 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 14:55:49 +0200 |
| commit | dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (patch) | |
| tree | 33fdd7c2eb44e54e7777e2d074127b129c5385ac /plugins/funind/recdef.ml | |
| parent | d2533da244f770261478ae829167cb3a8ad38038 (diff) | |
Remove some occurrences of Evd.empty
We address the easy ones, but they should probably be all removed.
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) |