diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index ca77e10c8d..a8b13e8456 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -229,6 +229,7 @@ let clenv_dependent hyps_only clenv = let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in let deps = dependent_metas clenv mvs ctyp_mvs in let nonlinear = duplicated_metas (clenv_value clenv) in + let ctyp_mvs = dependent_metas clenv (Metaset.elements ctyp_mvs) ctyp_mvs in (* Make the assumption that duplicated metas have internal dependencies *) List.filter (fun mv -> if Metaset.mem mv deps |