diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index d32d232fa..6449c183f 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -224,7 +224,7 @@ let keep_hyps env needed = | None -> Idset.empty | Some c -> global_vars_set env c in Idset.union - (global_vars_set env (body_of_type t)) + (global_vars_set env t) (Idset.union globc need) else need) ~init:needed |