diff options
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 09637d273..50a4703f6 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -403,8 +403,7 @@ let get_funs_constant mp dp = function const -> let find_constant_body const = match body_of_constant (Global.lookup_constant const) with - | Some b -> - let body = Lazyconstr.force b in + | Some body -> let body = Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) (Global.env ()) |