diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index b799c939f..47b8ca64b 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -47,7 +47,7 @@ let collect_meta_variables c = let check_no_metas clenv ccl = if occur_meta ccl then let metas = List.filter (fun na -> na<>Anonymous) - (List.map (Evd.meta_name clenv.env) (collect_meta_variables ccl)) in + (List.map (Evd.meta_name clenv.evd) (collect_meta_variables ccl)) in errorlabstrm "inversion" (str ("Cannot find an instantiation for variable"^ (if List.length metas = 1 then " " else "s ")) ++ |