diff options
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 18ef53276..5e72b8672 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -400,7 +400,7 @@ let get_funs_constant mp dp = match Global.body_of_constant const with | Some body -> let body = Tacred.cbv_norm_flags - (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) (Evd.from_env (Global.env ())) body |