diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/inv.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index e732a31c4c..140ddf8f43 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -45,8 +45,9 @@ 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.evd) (collect_meta_variables ccl)) in + let metas = List.filter (fun m -> not (Evd.meta_defined clenv.evd m)) + (collect_meta_variables ccl) in + let metas = List.map (Evd.meta_name clenv.evd) metas in errorlabstrm "inversion" (str ("Cannot find an instantiation for variable"^ (if List.length metas = 1 then " " else "s ")) ++ |