diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 072d664fcd..ed9d779ad7 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -231,7 +231,6 @@ let dependent_metas clenv mvs conclmetas = mvs conclmetas let clenv_dependent hyps_only clenv = - let mvs = collect_metas (clenv_value clenv) in let mvs = undefined_metas clenv.evd in let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in let deps = dependent_metas clenv mvs ctyp_mvs in |